1 /-
2 Copyright (c) 2018 Patrick Massot. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Normed spaces.
5
6 Authors: Patrick Massot, Johannes Hölzl
7 -/
8
9 import algebra.pi_instances
src └──────────────────┘
10 import linear_algebra.basic
src └──────────────────┘
11 import topology.instances.nnreal topology.instances.complex
src └───────────────────────┘ └────────────────────────┘
12 import topology.algebra.module
src └─────────────────────┘
13
14 variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}
15
16 noncomputable theory
17 open filter metric
18 open_locale topological_space
19 localized "notation f `→_{`:50 a `}`:0 b := filter.tendsto f (_root_.nhds a) (_root_.nhds b)" in filter
20
21 /-- Auxiliary class, endowing a type `α` with a function `norm : α → ℝ`. This class is designed to
22 be extended in more interesting classes specifying the properties of the norm. -/
23 class has_norm (α : Type*) := (norm : α → ℝ)
id └───┘ ┴ ┴ ┴
src ┴
typ └───┘ ┴ ┴ ┴
24
25 export has_norm (norm)
26
27 notation `∥`:1024 e:1 `∥`:1 := norm e
id └──┘
src └──┘
typ └──┘
28
29 section prio
30 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
31 /-- A normed group is an additive group endowed with a norm for which `dist x y = ∥x - y∥` defines
32 a metric space structure. -/
33 class normed_group (α : Type*) extends has_norm α, add_comm_group α, metric_space α :=
id └───┘ └──────┘ ┴ └────────────┘ ┴ └──────────┘ ┴
src └──────┘ └────────────┘ └──────────┘
typ └───┘ └──────┘ ┴ └────────────┘ ┴ └──────────┘ ┴
doc └──────┘ └──────────┘
34 (dist_eq : ∀ x y, dist x y = norm (x - y))
id ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
35 end prio
36
37 /-- Construct a normed group from a translation invariant distance -/
38 def normed_group.of_add_dist [has_norm α] [add_comm_group α] [metric_space α]
39 (H1 : ∀ x:α, ∥x∥ = dist x 0)
40 (H2 : ∀ x y z : α, dist x y ≤ dist (x + z) (y + z)) : normed_group α :=
id └┘ ┴
src └┘
typ └┘ ┴
doc └┘
41 { dist_eq := λ x y, begin
id ┴ ┴
typ ┴ ┴
st └─────
42 rw H1, apply le_antisymm,
id └┘ └─────────┘
src └─┘ └────┘└─────────┘
typ └─┘└┘ └────┘└─────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st ────────┘└─────────────────┘└─
43 { rw [sub_eq_add_neg, ← add_right_neg y], apply H2 },
id └────────────┘ └───────────┘ ┴
src └──┘└────────────┘└──┘└───────────┘┴ ┴ └────┘ ┴
typ └──┘└────────────┘└──┘└───────────┘┴┴┴ └────┘ ┴
doc └──┘ └──┘ ┴ ┴ └────┘ ┴
txt └──┘ └──┘ ┴ ┴ └────┘ ┴
par └──┘ └──┘ ┴ ┴ └────┘ ┴
pid └┘ └──┘ ┴ ┴ ┴ ┴
st ─────┘└────────────────┘└─────────────────┘└──────────┘└┘└
44 { have := H2 (x-y) 0 y, rwa [sub_add_cancel, zero_add] at this }
id └┘ ┴┴ ┴ └────────────┘ └──────┘
src └──────┘ ┴ ┴ └──┘ └───┘└────────────┘└┘└──────┘└────────┘
typ └──────┘└┘┴ ┴┴ └──┘┴ └───┘└────────────┘└┘└──────┘└────────┘
doc └──────┘ ┴ └──┘ └───┘ └┘ └────────┘
txt └──────┘ ┴ └──┘ └───┘ └┘ └────────┘
par └──────┘ ┴ └──┘ └───┘ └┘ └────────┘
pid └───┘└─┘ ┴ └──┘ └┘ └┘ ┴└──────┘┴
st ─────────────────────────┘└───────────────────┘└────────┘┴└───────┘└─
45 end }
st ────┘
46
47 /-- Construct a normed group from a translation invariant distance -/
48 def normed_group.of_add_dist' [has_norm α] [add_comm_group α] [metric_space α]
id └──────┘ ┴ └────────────┘ ┴ └──────────┘ ┴
src └──────┘ └────────────┘ └──────────┘
typ └──────┘ ┴ └────────────┘ ┴ └──────────┘ ┴
doc └──────┘ └──────────┘
49 (H1 : ∀ x:α, ∥x∥ = dist x 0)
id ┴ ┴┴┴ ┴ └──┘ ┴
src ┴ ┴ ┴ └──┘
typ ┴ ┴┴┴ ┴ └──┘ ┴
50 (H2 : ∀ x y z : α, dist (x + z) (y + z) ≤ dist x y) : normed_group α :=
id ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────────┘ ┴
src └──┘ ┴ ┴ ┴ └──┘ └──────────┘
typ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘
51 { dist_eq := λ x y, begin
id ┴ ┴
typ ┴ ┴
st └─────
52 rw H1, apply le_antisymm,
id └┘ └─────────┘
src └─┘ └────┘└─────────┘
typ └─┘└┘ └────┘└─────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st ────────┘└─────────────────┘└─
53 { have := H2 (x-y) 0 y, rwa [sub_add_cancel, zero_add] at this },
id └┘ ┴┴ ┴ └────────────┘ └──────┘
src └──────┘ ┴ ┴ └──┘ └───┘└────────────┘└┘└──────┘└────────┘
typ └──────┘└┘┴ ┴┴ └──┘┴ └───┘└────────────┘└┘└──────┘└────────┘
doc └──────┘ ┴ └──┘ └───┘ └┘ └────────┘
txt └──────┘ ┴ └──┘ └───┘ └┘ └────────┘
par └──────┘ ┴ └──┘ └───┘ └┘ └────────┘
pid └───┘└─┘ ┴ └──┘ └┘ └┘ ┴└──────┘┴
st ─────┘└──────────────────┘└───────────────────┘└────────┘┴└───────┘└┘└
54 { rw [sub_eq_add_neg, ← add_right_neg y], apply H2 }
id └────────────┘ └───────────┘ ┴
src └──┘└────────────┘└──┘└───────────┘┴ ┴ └────┘ ┴
typ └──┘└────────────┘└──┘└───────────┘┴┴┴ └────┘ ┴
doc └──┘ └──┘ ┴ ┴ └────┘ ┴
txt └──┘ └──┘ ┴ ┴ └────┘ ┴
par └──┘ └──┘ ┴ ┴ └────┘ ┴
pid └┘ └──┘ ┴ ┴ ┴ ┴
st ───────────────────────┘└─────────────────┘└──────────┘└─
55 end }
st ────┘
56
57 /-- A normed group can be built from a norm that satisfies algebraic properties. This is
58 formalised in this structure. -/
59 structure normed_group.core (α : Type*) [add_comm_group α] [has_norm α] : Prop :=
id └───┘ └────────────┘ ┴ └──────┘ ┴
src └────────────┘ └──────┘
typ └───┘ └────────────┘ ┴ └──────┘ ┴
doc └──────┘
60 (norm_eq_zero_iff : ∀ x : α, ∥x∥ = 0 ↔ x = 0)
id ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴
61 (triangle : ∀ x y : α, ∥x + y∥ ≤ ∥x∥ + ∥y∥)
id ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
62 (norm_neg : ∀ x : α, ∥-x∥ = ∥x∥)
id ┴ ┴ ┴┴┴┴ ┴ ┴┴┴
src ┴┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴┴ ┴ ┴┴┴
63
64 /-- Constructing a normed group from core properties of a norm, i.e., registering the distance and
65 the metric space structure from the norm properties. -/
66 noncomputable def normed_group.of_core (α : Type*) [add_comm_group α] [has_norm α]
id └────────────┘ ┴ └──────┘ ┴
src └────────────┘ └──────┘
typ └────────────┘ ┴ └──────┘ ┴
doc └──────┘
67 (C : normed_group.core α) : normed_group α :=
id └───────────────┘ ┴ └──────────┘ ┴
src └───────────────┘ └──────────┘
typ └───────────────┘ ┴ └──────────┘ ┴
doc └───────────────┘ └──────────┘
68 { dist := λ x y, ∥x - y∥,
id ┴ ┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴┴
69 dist_eq := assume x y, by refl,
id ┴ ┴
src └──┘
typ ┴ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
70 dist_self := assume x, (C.norm_eq_zero_iff (x - x)).mpr (show x - x = 0, by simp),
id ┴ ┴└───────────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ └─┘ ┴ ┴ └──┘
typ ┴ ┴└───────────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
71 eq_of_dist_eq_zero := assume x y h, show (x = y), from sub_eq_zero.mp $ (C.norm_eq_zero_iff (x - y)).mp h,
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└─┘ ┴└───────────────┘ ┴ ┴ ┴ └┘ ┴
src ┴ └─────────┘└─┘ └───────────────┘ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘└─┘ ┴└───────────────┘ ┴ ┴ ┴ └┘ ┴
72 dist_triangle := assume x y z,
id ┴ ┴ ┴
typ ┴ ┴ ┴
73 calc ∥x - z∥ = ∥x - y + (y - z)∥ : by simp
id ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
typ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
74 ... ≤ ∥x - y∥ + ∥y - z∥ : C.triangle _ _,
id ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴└───────┘
src ───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
typ ───────────┘ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴└───────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ───────────┘
st ───────────┘
75 dist_comm := assume x y,
id ┴ ┴
typ ┴ ┴
76 calc ∥x - y∥ = ∥ -(y - x)∥ : by simp
id ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
typ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
77 ... = ∥y - x∥ : by { rw [C.norm_neg] } }
id ┴┴ ┴ ┴┴
src ────────────┘ ┴ ┴ ┴ └──┘ └┘
typ ────────────┘ ┴┴ ┴ ┴┴ └──┘└────────┘└┘
doc ────────────┘ └──┘ └┘
txt ────────────┘ └──┘ └┘
par ────────────┘ └──┘ └┘
pid ────────────┘ └┘ ┴┴
st ────────────┘ └───────────────┘┴┴└┘
78
79 section normed_group
80 variables [normed_group α] [normed_group β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
81
82 lemma dist_eq_norm (g h : α) : dist g h = ∥g - h∥ :=
id ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └──┘ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴┴
83 normed_group.dist_eq _ _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
84
85 @[simp] lemma dist_zero_right (g : α) : dist g 0 = ∥g∥ :=
id ┴ └──┘ ┴ ┴ ┴┴┴
src └──┘ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴┴┴
doc └──┘
86 by rw [dist_eq_norm, sub_zero]
id └──────────┘ └──────┘
src └──┘└──────────┘└┘└──────┘└─
typ └──┘└──────────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────────┘└────────┘┴└
87
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
88 lemma norm_sub_rev (g h : α) : ∥g - h∥ = ∥h - g∥ :=
id ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴
89 by simpa only [dist_eq_norm] using dist_comm g h
id └──────────┘ └───────┘ ┴ ┴
src └──────────┘└──────────┘└──────┘└───────┘┴ ┴ └
typ └──────────┘└──────────┘└──────┘└───────┘┴┴┴┴└
doc └──────────┘ └──────┘ ┴ ┴ └
txt └──────────┘ └──────┘ ┴ ┴ └
par └──────────┘ └──────┘ ┴ ┴ └
pid ┴└──┘└┘ ┴┴└────┘ ┴ ┴ └
st └──────────────────────────────────────────────
90
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
91 @[simp] lemma norm_neg (g : α) : ∥-g∥ = ∥g∥ :=
id ┴ ┴┴┴┴ ┴ ┴┴┴
src ┴┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴┴ ┴ ┴┴┴
doc └──┘
92 by simpa using norm_sub_rev 0 g
id └──────────┘ ┴
src └──────────┘└──────────┘└─┘ └
typ └──────────┘└──────────┘└─┘┴└
doc └──────────┘ └─┘ └
txt └──────────┘ └─┘ └
par └──────────┘ └─┘ └
pid ┴└────┘ └─┘ └
st └─────────────────────────────
93
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
94 @[simp] lemma dist_add_left (g h₁ h₂ : α) : dist (g + h₁) (g + h₂) = dist h₁ h₂ :=
id ┴ └──┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └┘ └┘
src └──┘ ┴ ┴ ┴ └──┘
typ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └┘ └┘
doc └──┘
95 by simp [dist_eq_norm]
id └──────────┘
src └────┘└──────────┘└─
typ └────┘└──────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────
96
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
97 @[simp] lemma dist_add_right (g₁ g₂ h : α) : dist (g₁ + h) (g₂ + h) = dist g₁ g₂ :=
id ┴ └──┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ └┘
src └──┘ ┴ ┴ ┴ └──┘
typ ┴ └──┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ └┘
doc └──┘
98 by simp [dist_eq_norm]
id └──────────┘
src └────┘└──────────┘└─
typ └────┘└──────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────
99
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
100 @[simp] lemma dist_neg_neg (g h : α) : dist (-g) (-h) = dist g h :=
id ┴ └──┘ ┴┴ ┴┴ ┴ └──┘ ┴ ┴
src └──┘ ┴ ┴ ┴ └──┘
typ ┴ └──┘ ┴┴ ┴┴ ┴ └──┘ ┴ ┴
doc └──┘
101 by simp only [dist_eq_norm, neg_sub_neg, norm_sub_rev]
id └──────────┘ └─────────┘ └──────────┘
src └─────────┘└──────────┘└┘└─────────┘└┘└──────────┘└─
typ └─────────┘└──────────┘└┘└─────────┘└┘└──────────┘└─
doc └─────────┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────
102
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
103 @[simp] lemma dist_sub_left (g h₁ h₂ : α) : dist (g - h₁) (g - h₂) = dist h₁ h₂ :=
id ┴ └──┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └┘ └┘
src └──┘ ┴ ┴ ┴ └──┘
typ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └┘ └┘
doc └──┘
104 by simp only [sub_eq_add_neg, dist_add_left, dist_neg_neg]
id └────────────┘ └───────────┘ └──────────┘
src └─────────┘└────────────┘└┘└───────────┘└┘└──────────┘└─
typ └─────────┘└────────────┘└┘└───────────┘└┘└──────────┘└─
doc └─────────┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────
105
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
106 @[simp] lemma dist_sub_right (g₁ g₂ h : α) : dist (g₁ - h) (g₂ - h) = dist g₁ g₂ :=
id ┴ └──┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ └┘
src └──┘ ┴ ┴ ┴ └──┘
typ ┴ └──┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘ └┘
doc └──┘
107 dist_add_right _ _ _
id └────────────┘
src └────────────┘
typ └────────────┘
108
109 /-- Triangle inequality for the norm. -/
110 lemma norm_add_le (g h : α) : ∥g + h∥ ≤ ∥g∥ + ∥h∥ :=
id ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
111 by simpa [dist_eq_norm] using dist_triangle g 0 (-h)
id └──────────┘ └───────────┘ ┴ ┴┴
src └─────┘└──────────┘└──────┘└───────────┘┴ └─┘ ┴ └─
typ └─────┘└──────────┘└──────┘└───────────┘┴┴└─┘ ┴┴└─
doc └─────┘ └──────┘ ┴ └─┘ └─
txt └─────┘ └──────┘ ┴ └─┘ └─
par └─────┘ └──────┘ ┴ └─┘ └─
pid ┴┴ ┴┴└────┘ ┴ └─┘ ┴└
st └──────────────────────────────────────────────────
112
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
113 lemma norm_add_le_of_le {g₁ g₂ : α} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :
id ┴ ┴ ┴└┘┴ ┴ └┘ ┴└┘┴ ┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴└┘┴ ┴ └┘ ┴└┘┴ ┴ └┘
114 ∥g₁ + g₂∥ ≤ n₁ + n₂ :=
id ┴└┘ ┴ └┘┴ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ ┴└┘ ┴ └┘┴ ┴ └┘ ┴ └┘
115 le_trans (norm_add_le g₁ g₂) (add_le_add H₁ H₂)
id └──────┘ └─────────┘ └┘ └┘ └────────┘ └┘ └┘
src └──────┘ └─────────┘ └────────┘
typ └──────┘ └─────────┘ └┘ └┘ └────────┘ └┘ └┘
doc └─────────┘
116
117 lemma dist_add_add_le (g₁ g₂ h₁ h₂ : α) :
id ┴
typ ┴
118 dist (g₁ + g₂) (h₁ + h₂) ≤ dist g₁ h₁ + dist g₂ h₂ :=
id └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘
src └──┘ ┴ ┴ ┴ └──┘ ┴ └──┘
typ └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘
119 by simpa only [dist_add_left, dist_add_right] using dist_triangle (g₁ + g₂) (h₁ + g₂) (h₁ + h₂)
id └───────────┘ └────────────┘ └───────────┘ └┘ ┴ └┘ └┘ └┘
src └──────────┘└───────────┘└┘└────────────┘└──────┘└───────────┘┴ ┴┴┴ └┘ ┴ ┴ └┘ ┴ ┴ └─
typ └──────────┘└───────────┘└┘└────────────┘└──────┘└───────────┘┴ └┘┴┴┴ └┘ ┴ ┴└┘└┘ └┘┴ ┴└┘└─
doc └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─
txt └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─
par └──────────┘ └┘ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─
pid ┴└──┘└┘ └┘ ┴┴└────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴└
st └─────────────────────────────────────────────────────────────────────────────────────────────
120
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
121 lemma dist_add_add_le_of_le {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : ℝ}
id ┴ ┴
src ┴
typ ┴ ┴
122 (H₁ : dist g₁ h₁ ≤ d₁) (H₂ : dist g₂ h₂ ≤ d₂) :
id └──┘ └┘ └┘ ┴ └┘ └──┘ └┘ └┘ ┴ └┘
src └──┘ ┴ └──┘ ┴
typ └──┘ └┘ └┘ ┴ └┘ └──┘ └┘ └┘ ┴ └┘
123 dist (g₁ + g₂) (h₁ + h₂) ≤ d₁ + d₂ :=
id └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
124 le_trans (dist_add_add_le g₁ g₂ h₁ h₂) (add_le_add H₁ H₂)
id └──────┘ └─────────────┘ └┘ └┘ └┘ └┘ └────────┘ └┘ └┘
src └──────┘ └─────────────┘ └────────┘
typ └──────┘ └─────────────┘ └┘ └┘ └┘ └┘ └────────┘ └┘ └┘
125
126 lemma dist_sub_sub_le (g₁ g₂ h₁ h₂ : α) :
id ┴
typ ┴
127 dist (g₁ - g₂) (h₁ - h₂) ≤ dist g₁ h₁ + dist g₂ h₂ :=
id └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘
src └──┘ ┴ ┴ ┴ └──┘ ┴ └──┘
typ └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘
128 dist_neg_neg g₂ h₂ ▸ dist_add_add_le _ _ _ _
id └──────────┘ └┘ └┘ ┴ └─────────────┘
src └──────────┘ ┴ └─────────────┘
typ └──────────┘ └┘ └┘ ┴ └─────────────┘
129
130 lemma dist_sub_sub_le_of_le {g₁ g₂ h₁ h₂ : α} {d₁ d₂ : ℝ}
id ┴ ┴
src ┴
typ ┴ ┴
131 (H₁ : dist g₁ h₁ ≤ d₁) (H₂ : dist g₂ h₂ ≤ d₂) :
id └──┘ └┘ └┘ ┴ └┘ └──┘ └┘ └┘ ┴ └┘
src └──┘ ┴ └──┘ ┴
typ └──┘ └┘ └┘ ┴ └┘ └──┘ └┘ └┘ ┴ └┘
132 dist (g₁ - g₂) (h₁ - h₂) ≤ d₁ + d₂ :=
id └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
src └──┘ ┴ ┴ ┴ ┴
typ └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘
133 le_trans (dist_sub_sub_le g₁ g₂ h₁ h₂) (add_le_add H₁ H₂)
id └──────┘ └─────────────┘ └┘ └┘ └┘ └┘ └────────┘ └┘ └┘
src └──────┘ └─────────────┘ └────────┘
typ └──────┘ └─────────────┘ └┘ └┘ └┘ └┘ └────────┘ └┘ └┘
134
135 @[simp] lemma norm_nonneg (g : α) : 0 ≤ ∥g∥ :=
id ┴ ┴ ┴┴┴
src ┴ ┴ ┴
typ ┴ ┴ ┴┴┴
doc └──┘
136 by { rw[←dist_zero_right], exact dist_nonneg }
id └─────────────┘ └─────────┘
src └──┘└─────────────┘┴ └────┘└─────────┘┴
typ └──┘└─────────────┘┴ └────┘└─────────┘┴
doc └──┘ ┴ └────┘ ┴
txt └──┘ ┴ └────┘ ┴
par └──┘ ┴ └────┘ ┴
pid └┘ ┴ ┴ ┴
st └────────────────────┘└───────────────────┘└┘
137
138 lemma norm_eq_zero (g : α) : ∥g∥ = 0 ↔ g = 0 :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴
139 by { rw[←dist_zero_right], exact dist_eq_zero }
id └─────────────┘ └──────────┘
src └──┘└─────────────┘┴ └────┘└──────────┘┴
typ └──┘└─────────────┘┴ └────┘└──────────┘┴
doc └──┘ ┴ └────┘ ┴
txt └──┘ ┴ └────┘ ┴
par └──┘ ┴ └────┘ ┴
pid └┘ ┴ ┴ ┴
st └────────────────────┘└────────────────────┘└┘
140
141 @[simp] lemma norm_zero : ∥(0:α)∥ = 0 := (norm_eq_zero _).2 rfl
id ┴ ┴ ┴ ┴ └──────────┘ ┴ └─┘
src ┴ ┴ ┴ └──────────┘ ┴ └─┘
typ ┴ ┴ ┴ ┴ └──────────┘ ┴ └─┘
doc └──┘
142
143 lemma norm_sum_le {β} : ∀(s : finset β) (f : β → α), ∥s.sum f∥ ≤ s.sum (λa, ∥ f a ∥) :=
id └────┘ ┴ ┴ ┴ ┴ ┴┴└──┘ ┴┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴┴└──┘ ┴┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴
doc └────┘
144 finset.le_sum_of_subadditive norm norm_zero norm_add_le
id └──────────────────────────┘ └──┘ └───────┘ └─────────┘
src └──────────────────────────┘ └──┘ └───────┘ └─────────┘
typ └──────────────────────────┘ └──┘ └───────┘ └─────────┘
doc └─────────┘
145
146 lemma norm_sum_le_of_le {β} (s : finset β) {f : β → α} {n : β → ℝ} (h : ∀ b ∈ s, ∥f b∥ ≤ n b) :
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └────┘
147 ∥s.sum f∥ ≤ s.sum n :=
id ┴┴└──┘ ┴┴ ┴ ┴└──┘ ┴
src ┴ └──┘ ┴ ┴ └──┘
typ ┴┴└──┘ ┴┴ ┴ ┴└──┘ ┴
148 by { haveI := classical.dec_eq β, exact le_trans (norm_sum_le s f) (finset.sum_le_sum h) }
id └──────────────┘ ┴ └──────┘ └─────────┘ ┴ ┴ └───────────────┘ ┴
src └───────┘└──────────────┘┴ └────┘└──────┘┴ └─────────┘┴ ┴ └┘ └───────────────┘┴ └┘
typ └───────┘└──────────────┘┴┴ └────┘└──────┘┴ └─────────┘┴┴┴┴└┘ └───────────────┘┴┴└┘
doc └───────┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ └┘
txt └───────┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ └┘
par └───────┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ └┘
pid ┴└─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴
st └────────────────────────────┘└───────────────────────────────────────────────────────┘└┘
149
150 lemma norm_pos_iff (g : α) : 0 < ∥ g ∥ ↔ g ≠ 0 :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
151 dist_zero_right g ▸ dist_pos
id └─────────────┘ ┴ ┴ └──────┘
src └─────────────┘ ┴ └──────┘
typ └─────────────┘ ┴ ┴ └──────┘
152
153 lemma norm_le_zero_iff (g : α) : ∥g∥ ≤ 0 ↔ g = 0 :=
id ┴ ┴┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴
154 by { rw[←dist_zero_right], exact dist_le_zero }
id └─────────────┘ └──────────┘
src └──┘└─────────────┘┴ └────┘└──────────┘┴
typ └──┘└─────────────┘┴ └────┘└──────────┘┴
doc └──┘ ┴ └────┘ ┴
txt └──┘ ┴ └────┘ ┴
par └──┘ ┴ └────┘ ┴
pid └┘ ┴ ┴ ┴
st └────────────────────┘└────────────────────┘└┘
155
156 lemma norm_sub_le (g h : α) : ∥g - h∥ ≤ ∥g∥ + ∥h∥ :=
id ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
157 by simpa [dist_eq_norm] using dist_triangle g 0 h
id └──────────┘ └───────────┘ ┴ ┴
src └─────┘└──────────┘└──────┘└───────────┘┴ └─┘ └
typ └─────┘└──────────┘└──────┘└───────────┘┴┴└─┘┴└
doc └─────┘ └──────┘ ┴ └─┘ └
txt └─────┘ └──────┘ ┴ └─┘ └
par └─────┘ └──────┘ ┴ └─┘ └
pid ┴┴ ┴┴└────┘ ┴ └─┘ └
st └───────────────────────────────────────────────
158
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
159 lemma norm_sub_le_of_le {g₁ g₂ : α} {n₁ n₂ : ℝ} (H₁ : ∥g₁∥ ≤ n₁) (H₂ : ∥g₂∥ ≤ n₂) :
id ┴ ┴ ┴└┘┴ ┴ └┘ ┴└┘┴ ┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴└┘┴ ┴ └┘ ┴└┘┴ ┴ └┘
160 ∥g₁ - g₂∥ ≤ n₁ + n₂ :=
id ┴└┘ ┴ └┘┴ ┴ └┘ ┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ ┴└┘ ┴ └┘┴ ┴ └┘ ┴ └┘
161 le_trans (norm_sub_le g₁ g₂) (add_le_add H₁ H₂)
id └──────┘ └─────────┘ └┘ └┘ └────────┘ └┘ └┘
src └──────┘ └─────────┘ └────────┘
typ └──────┘ └─────────┘ └┘ └┘ └────────┘ └┘ └┘
162
163 lemma dist_le_norm_add_norm (g h : α) : dist g h ≤ ∥g∥ + ∥h∥ :=
id ┴ └──┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴┴
164 by { rw dist_eq_norm, apply norm_sub_le }
id └──────────┘ └─────────┘
src └─┘└──────────┘ └────┘└─────────┘┴
typ └─┘└──────────┘ └────┘└─────────┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └────────────────┘└──────────────────┘└┘
165
166 lemma abs_norm_sub_norm_le (g h : α) : abs(∥g∥ - ∥h∥) ≤ ∥g - h∥ :=
id ┴ └─┘ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴
167 by simpa [dist_eq_norm] using abs_dist_sub_le g h 0
id └──────────┘ └─────────────┘ ┴ ┴
src └─────┘└──────────┘└──────┘└─────────────┘┴ ┴ └──
typ └─────┘└──────────┘└──────┘└─────────────┘┴┴┴┴└──
doc └─────┘ └──────┘ ┴ ┴ └──
txt └─────┘ └──────┘ ┴ ┴ └──
par └─────┘ └──────┘ ┴ ┴ └──
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴└─
st └─────────────────────────────────────────────────
168
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
169 lemma norm_sub_norm_le (g h : α) : ∥g∥ - ∥h∥ ≤ ∥g - h∥ :=
id ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴
170 le_trans (le_abs_self _) (abs_norm_sub_norm_le g h)
id └──────┘ └─────────┘ └──────────────────┘ ┴ ┴
src └──────┘ └─────────┘ └──────────────────┘
typ └──────┘ └─────────┘ └──────────────────┘ ┴ ┴
171
172 lemma dist_norm_norm_le (g h : α) : dist ∥g∥ ∥h∥ ≤ ∥g - h∥ :=
id ┴ └──┘ ┴┴┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴
src └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴┴┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴
173 abs_norm_sub_norm_le g h
id └──────────────────┘ ┴ ┴
src └──────────────────┘
typ └──────────────────┘ ┴ ┴
174
175 lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
id ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴┴┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴┴┴ ┴ ┴
doc └──┘
176 set.ext $ assume a, by simp
id └─────┘ ┴
src └─────┘ └────
typ └─────┘ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
177
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
178 lemma norm_le_of_mem_closed_ball {g h : α} {r : ℝ} (H : h ∈ closed_ball g r) :
id ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
src ┴ ┴ └─────────┘
typ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └─────────┘
179 ∥h∥ ≤ ∥g∥ + r :=
id ┴┴┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴┴┴ ┴ ┴
180 calc
181 ∥h∥ = ∥g + (h - g)∥ : by { congr' 1, abel }
id ┴┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └───┘
typ ┴┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └───┘
doc └──────┘ └───┘
txt └──────┘ └───┘
par └──────┘ └───┘
pid ┴┴ ┴
st └─────────┘└─────┘└┘
182 ... ≤ ∥g∥ + ∥h - g∥ : norm_add_le _ _
id ┴┴┴ ┴ ┴┴ ┴ ┴┴ └─────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
typ ┴┴┴ ┴ ┴┴ ┴ ┴┴ └─────────┘
doc └─────────┘
183 ... ≤ ∥g∥ + r : by { apply add_le_add_left, rw ← dist_eq_norm, exact H }
id ┴┴┴ ┴ ┴ └─────────────┘ └──────────┘ ┴
src ┴ ┴ ┴ └────┘└─────────────┘ └───┘└──────────┘ └────┘ ┴
typ ┴┴┴ ┴ ┴ └────┘└─────────────┘ └───┘└──────────┘ └────┘┴┴
doc └────┘ └───┘ └────┘ ┴
txt └────┘ └───┘ └────┘ ┴
par └────┘ └───┘ └────┘ ┴
pid ┴ └─┘ ┴ ┴
st └──────────────────────┘└─────────────────┘└────────┘└┘
184
185 lemma norm_lt_of_mem_ball {g h : α} {r : ℝ} (H : h ∈ ball g r) :
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘
186 ∥h∥ < ∥g∥ + r :=
id ┴┴┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴┴┴ ┴ ┴
187 calc
188 ∥h∥ = ∥g + (h - g)∥ : by { congr' 1, abel }
id ┴┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └───┘
typ ┴┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └──────┘ └───┘
doc └──────┘ └───┘
txt └──────┘ └───┘
par └──────┘ └───┘
pid ┴┴ ┴
st └─────────┘└─────┘└┘
189 ... ≤ ∥g∥ + ∥h - g∥ : norm_add_le _ _
id ┴┴┴ ┴ ┴┴ ┴ ┴┴ └─────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ └─────────┘
typ ┴┴┴ ┴ ┴┴ ┴ ┴┴ └─────────┘
doc └─────────┘
190 ... < ∥g∥ + r : by { apply add_lt_add_left, rw ← dist_eq_norm, exact H }
id ┴┴┴ ┴ ┴ └─────────────┘ └──────────┘ ┴
src ┴ ┴ ┴ └────┘└─────────────┘ └───┘└──────────┘ └────┘ ┴
typ ┴┴┴ ┴ ┴ └────┘└─────────────┘ └───┘└──────────┘ └────┘┴┴
doc └────┘ └───┘ └────┘ ┴
txt └────┘ └───┘ └────┘ ┴
par └────┘ └───┘ └────┘ ┴
pid ┴ └─┘ ┴ ┴
st └──────────────────────┘└─────────────────┘└────────┘└┘
191
192 theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
id ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ └────┘ ┴
193 tendsto f l (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in l, ∥ f x ∥ < ε :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └┘ └┘ ┴
194 metric.tendsto_nhds.trans $ forall_congr $ λ ε, forall_congr $ λ εgt0,
id └─────────────────┘└────┘ └──────────┘ ┴ └──────────┘ └──┘
src └─────────────────┘└────┘ └──────────┘ └──────────┘
typ └─────────────────┘└────┘ └──────────┘ ┴ └──────────┘ └──┘
195 begin
st └─────
196 simp only [dist_zero_right],
id └─────────────┘
src └─────────┘└─────────────┘┴
typ └─────────┘└─────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ────────────────────────────┘└─
197 exact exists_sets_subset_iff
id └────────────────────┘
src └────┘└────────────────────┘┴
typ └────┘└────────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────┘
198 end
st └─┘
199
200 section nnnorm
201
202 /-- Version of the norm taking values in nonnegative reals. -/
203 def nnnorm (a : α) : nnreal := ⟨norm a, norm_nonneg a⟩
id ┴ └────┘ └──┘ ┴ └─────────┘ ┴
src └────┘ └──┘ └─────────┘
typ ┴ └────┘ └──┘ ┴ └─────────┘ ┴
doc └────┘
204
205 @[simp] lemma coe_nnnorm (a : α) : (nnnorm a : ℝ) = norm a := rfl
id ┴ └────┘ ┴ ┴ ┴ └──┘ ┴ └─┘
src └────┘ ┴ ┴ └──┘ └─┘
typ ┴ └────┘ ┴ ┴ ┴ └──┘ ┴ └─┘
doc └──┘ └────┘
206
207 lemma nndist_eq_nnnorm (a b : α) : nndist a b = nnnorm (a - b) := nnreal.eq $ dist_eq_norm _ _
id ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └───────┘ └──────────┘
src └────┘ ┴ └────┘ ┴ └───────┘ └──────────┘
typ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └───────┘ └──────────┘
doc └────┘ └────┘
208
209 lemma nnnorm_eq_zero (a : α) : nnnorm a = 0 ↔ a = 0 :=
id ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴
typ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘
210 by simp only [nnreal.eq_iff.symm, nnreal.coe_zero, coe_nnnorm, norm_eq_zero]
id └─────────────┘ └────────┘ └──────────┘
src └─────────┘ └┘└─────────────┘└┘└────────┘└┘└──────────┘└─
typ └─────────┘└────────────────┘└┘└─────────────┘└┘└────────┘└┘└──────────┘└─
doc └─────────┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ ┴└
st └──────────────────────────────────────────────────────────────────────────
211
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
212 @[simp] lemma nnnorm_zero : nnnorm (0 : α) = 0 :=
id └────┘ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴
doc └──┘ └────┘
213 nnreal.eq norm_zero
id └───────┘ └───────┘
src └───────┘ └───────┘
typ └───────┘ └───────┘
214
215 lemma nnnorm_add_le (g h : α) : nnnorm (g + h) ≤ nnnorm g + nnnorm h :=
id ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
src └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
doc └────┘ └────┘ └────┘
216 nnreal.coe_le.2 $ norm_add_le g h
id └───────────┘┴ └─────────┘ ┴ ┴
src └───────────┘┴ └─────────┘
typ └───────────┘┴ └─────────┘ ┴ ┴
doc └─────────┘
217
218 @[simp] lemma nnnorm_neg (g : α) : nnnorm (-g) = nnnorm g :=
id ┴ └────┘ ┴┴ ┴ └────┘ ┴
src └────┘ ┴ ┴ └────┘
typ ┴ └────┘ ┴┴ ┴ └────┘ ┴
doc └──┘ └────┘ └────┘
219 nnreal.eq $ norm_neg g
id └───────┘ └──────┘ ┴
src └───────┘ └──────┘
typ └───────┘ └──────┘ ┴
220
221 lemma nndist_nnnorm_nnnorm_le (g h : α) : nndist (nnnorm g) (nnnorm h) ≤ nnnorm (g - h) :=
id ┴ └────┘ └────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘ └────┘ └────┘ ┴ └────┘ ┴
typ ┴ └────┘ └────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────┘ └────┘ └────┘ └────┘
222 nnreal.coe_le.2 $ dist_norm_norm_le g h
id └───────────┘┴ └───────────────┘ ┴ ┴
src └───────────┘┴ └───────────────┘
typ └───────────┘┴ └───────────────┘ ┴ ┴
223
224 lemma of_real_norm_eq_coe_nnnorm (x : β) : ennreal.of_real ∥x∥ = (nnnorm x : ennreal) :=
id ┴ └─────────────┘ ┴┴┴ ┴ └────┘ ┴ └─────┘
src └─────────────┘ ┴ ┴ ┴ └────┘ └─────┘
typ ┴ └─────────────┘ ┴┴┴ ┴ └────┘ ┴ └─────┘
doc └─────────────┘ └────┘ └─────┘
225 ennreal.of_real_eq_coe_nnreal _
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
226
227 lemma edist_eq_coe_nnnorm (x : β) : edist x 0 = (nnnorm x : ennreal) :=
id ┴ └───┘ ┴ ┴ └────┘ ┴ └─────┘
src └───┘ ┴ └────┘ └─────┘
typ ┴ └───┘ ┴ ┴ └────┘ ┴ └─────┘
doc └────┘ └─────┘
228 by { rw [edist_dist, dist_eq_norm, _root_.sub_zero, of_real_norm_eq_coe_nnnorm] }
id └────────┘ └──────────┘ └─────────────┘ └────────────────────────┘
src └──┘└────────┘└┘└──────────┘└┘└─────────────┘└┘└────────────────────────┘└┘
typ └──┘└────────┘└┘└──────────┘└┘└─────────────┘└┘└────────────────────────┘└┘
doc └──┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ ┴┴
st └───────────────┘└────────────┘└───────────────┘└──────────────────────────┘┴┴└┘
229
230 end nnnorm
231
232 /-- A submodule of a normed group is also a normed group, with the restriction of the norm.
233 As all instances can be inferred from the submodule `s`, they are put as implicit instead of
234 typeclasses. -/
235 instance submodule.normed_group {𝕜 : Type*} {_ : ring 𝕜}
id └──┘ ┴
src └──┘
typ └──┘ ┴
236 {E : Type*} [normed_group E] {_ : module 𝕜 E} (s : submodule 𝕜 E) : normed_group s :=
id └──────────┘ ┴ └────┘ ┴ ┴ └───────┘ ┴ ┴ └──────────┘ ┴
src └──────────┘ └────┘ └───────┘ └──────────┘
typ └──────────┘ ┴ └────┘ ┴ ┴ └───────┘ ┴ ┴ └──────────┘ ┴
doc └──────────┘ └────┘ └───────┘ └──────────┘
237 { norm := λx, norm (x : E),
id ┴ └──┘ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴
238 dist_eq := λx y, dist_eq_norm (x : E) (y : E) }
id ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘
typ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
239
240 /-- normed group instance on the product of two normed groups, using the sup norm. -/
241 instance prod.normed_group : normed_group (α × β) :=
id └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴
doc └──────────┘
242 { norm := λx, max ∥x.1∥ ∥x.2∥,
id ┴ └─┘ ┴┴┴ ┴ ┴┴┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴┴┴ ┴ ┴┴┴ ┴
243 dist_eq := assume (x y : α × β),
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
244 show max (dist x.1 y.1) (dist x.2 y.2) = (max ∥(x - y).1∥ ∥(x - y).2∥), by simp [dist_eq_norm] }
id └─┘ └──┘ ┴┴ ┴┴ └──┘ ┴┴ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘
src └─┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────────┘└┘
typ └─┘ └──┘ ┴┴ ┴┴ └──┘ ┴┴ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └───────────────────┘
245
246 lemma norm_fst_le (x : α × β) : ∥x.1∥ ≤ ∥x∥ :=
id ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴
247 by simp [norm, le_max_left]
id └─────────┘
src └────┘ └┘└─────────┘└─
typ └────┘ └┘└─────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────────
248
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
249 lemma norm_snd_le (x : α × β) : ∥x.2∥ ≤ ∥x∥ :=
id ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴
250 by simp [norm, le_max_right]
id └──────────┘
src └────┘ └┘└──────────┘└─
typ └────┘ └┘└──────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────────────
251
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
252 /-- normed group instance on the product of finitely many normed groups, using the sup norm. -/
253 instance pi.normed_group {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] :
id ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴
src └─────┘ └──────────┘
typ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └─────┘ └──────────┘
254 normed_group (Πi, π i) :=
id └──────────┘ ┴ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ ┴
doc └──────────┘
255 { norm := λf, ((finset.sup finset.univ (λ b, nnnorm (f b)) : nnreal) : ℝ),
id ┴ └────────┘ └─────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴
src └────────┘ └─────────┘ └────┘ └────┘ ┴
typ ┴ └────────┘ └─────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴
doc └────────┘ └─────────┘ └────┘ └────┘
256 dist_eq := assume x y,
id ┴ ┴
typ ┴ ┴
257 congr_arg (coe : nnreal → ℝ) $ congr_arg (finset.sup finset.univ) $ funext $ assume a,
id └───────┘ └─┘ └────┘ ┴ └───────┘ └────────┘ └─────────┘ └────┘ ┴
src └───────┘ └─┘ └────┘ ┴ └───────┘ └────────┘ └─────────┘ └────┘
typ └───────┘ └─┘ └────┘ ┴ └───────┘ └────────┘ └─────────┘ └────┘ ┴
doc └────┘ └────────┘ └─────────┘
258 show nndist (x a) (y a) = nnnorm (x a - y a), from nndist_eq_nnnorm _ _ }
id └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └──────────────┘
src └────┘ ┴ └────┘ ┴ └──────────────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └──────────────┘
doc └────┘ └────┘
259
260 /-- The norm of an element in a product space is `≤ r` if and only if the norm of each
261 component is. -/
262 lemma pi_norm_le_iff {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] {r : ℝ} (hr : 0 ≤ r)
id ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──────────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──────────┘
263 {x : Πi, π i} : ∥x∥ ≤ r ↔ ∀i, ∥x i∥ ≤ r :=
id ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
264 by { simp only [(dist_zero_right _).symm, dist_pi_le_iff hr], refl }
id └─────────────┘ └────────────┘ └┘
src └─────────┘ └─────────────┘└────────┘└────────────┘┴ ┴ └───┘
typ └─────────┘ └─────────────┘└────────┘└────────────┘┴└┘┴ └───┘
doc └─────────┘ └────────┘ ┴ ┴ └───┘
txt └─────────┘ └────────┘ ┴ ┴ └───┘
par └─────────┘ └────────┘ ┴ ┴ └───┘
pid ┴└──┘└┘ └────────┘ ┴ ┴ ┴
st └────────────────────────────────────────────────────────┘└─────┘└┘
265
266 lemma norm_le_pi_norm {π : ι → Type*} [fintype ι] [∀i, normed_group (π i)] (x : Πi, π i) (i : ι) :
id ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └──────────┘
typ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └──────────┘
267 ∥x i∥ ≤ ∥x∥ :=
id ┴┴ ┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴┴ ┴ ┴┴┴
268 (pi_norm_le_iff (norm_nonneg x)).1 (le_refl _) i
id └────────────┘ └─────────┘ ┴ ┴ └─────┘ ┴
src └────────────┘ └─────────┘ ┴ └─────┘
typ └────────────┘ └─────────┘ ┴ ┴ └─────┘ ┴
doc └────────────┘
269
270 lemma tendsto_iff_norm_tendsto_zero {f : ι → β} {a : filter ι} {b : β} :
id ┴ ┴ └────┘ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴
271 tendsto f a (𝓝 b) ↔ tendsto (λ e, ∥ f e - b ∥) a (𝓝 0) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └─────┘ ┴
272 by rw tendsto_iff_dist_tendsto_zero ; simp only [(dist_eq_norm _ _).symm]
id └───────────────────────────┘ └──────────┘
src └─┘└───────────────────────────┘┴ └─────────┘ └──────────┘└───────────
typ └─┘└───────────────────────────┘┴ └─────────┘ └──────────┘└───────────
doc └─┘ ┴ └─────────┘ └───────────
txt └─┘ ┴ └─────────┘ └───────────
par └─┘ ┴ └─────────┘ └───────────
pid ┴ ┴ ┴└──┘└┘ └─────────┘└
st └───────────────────────────────────────────────────────────────────────
273
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
274 lemma tendsto_zero_iff_norm_tendsto_zero {f : γ → β} {a : filter γ} :
id ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ └────┘ ┴
275 tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥ f e ∥) a (𝓝 0) :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └─────┘ ┴
276 have tendsto f a (𝓝 0) ↔ tendsto (λ e, ∥ f e - 0 ∥) a (𝓝 0) :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └─────┘ ┴
277 tendsto_iff_norm_tendsto_zero,
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
278 by simpa
src └─────
typ └─────
doc └─────
txt └─────
par └─────
pid └
st └──────
279
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
280 lemma lim_norm (x : α) : (λg:α, ∥g - x∥) →_{x} 0 :=
id ┴ ┴ ┴┴ ┴ ┴┴ └─┘┴┴
src ┴ ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴┴ ┴ ┴┴ └─┘┴┴
doc └─┘ ┴
281 tendsto_iff_norm_tendsto_zero.1 (continuous_iff_continuous_at.1 continuous_id x)
id └───────────────────────────┘┴ └──────────────────────────┘┴ └───────────┘ ┴
src └───────────────────────────┘┴ └──────────────────────────┘┴ └───────────┘
typ └───────────────────────────┘┴ └──────────────────────────┘┴ └───────────┘ ┴
282
283 lemma lim_norm_zero : (λg:α, ∥g∥) →_{0} 0 :=
id ┴ ┴┴┴ └─┘ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴┴┴ └─┘ ┴
doc └─┘ ┴
284 by simpa using lim_norm (0:α)
id └──────┘ ┴
src └──────────┘└──────┘┴ └┘ └─
typ └──────────┘└──────┘┴ └┘┴└─
doc └──────────┘ ┴ └┘ └─
txt └──────────┘ ┴ └┘ └─
par └──────────┘ ┴ └┘ └─
pid ┴└────┘ ┴ └┘ ┴└
st └───────────────────────────
285
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
286 lemma continuous_norm : continuous (λg:α, ∥g∥) :=
id └────────┘ ┴ ┴┴┴
src └────────┘ ┴ ┴
typ └────────┘ ┴ ┴┴┴
doc └────────┘
287 begin
st └─────
288 rw continuous_iff_continuous_at,
id └──────────────────────────┘
src └─┘└──────────────────────────┘
typ └─┘└──────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────────────────┘└─
289 intro x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
290 rw [continuous_at, tendsto_iff_dist_tendsto_zero],
id └───────────┘ └───────────────────────────┘
src └──┘└───────────┘└┘└───────────────────────────┘┴
typ └──┘└───────────┘└┘└───────────────────────────┘┴
doc └──┘└───────────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────┘└─────────────────────────────┘└──
291 exact squeeze_zero (λ t, abs_nonneg _) (λ t, abs_norm_sub_norm_le _ _) (lim_norm x)
id └──────────┘ └────────┘ └──────────────────┘ └──────┘ ┴
src └────┘└──────────┘┴ └──┘└────────┘└──┘ └──┘└──────────────────┘└────┘ └──────┘┴ └┘
typ └────┘└──────────┘┴ └──┘└────────┘└──┘ └──┘└──────────────────┘└────┘ └──────┘┴┴└┘
doc └────┘ ┴ └──┘ └──┘ └──┘ └────┘ ┴ └┘
txt └────┘ ┴ └──┘ └──┘ └──┘ └────┘ ┴ └┘
par └────┘ ┴ └──┘ └──┘ └──┘ └────┘ ┴ └┘
pid ┴ ┴ └──┘ └──┘ └──┘ └────┘ ┴ ┴┴
st ─────────────────────────────────────────────────────────────────────────────────────┘
292 end
st └─┘
293
294 lemma filter.tendsto.norm {β : Type*} {l : filter β} {f : β → α} {a : α} (h : tendsto f l (𝓝 a)) :
id └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └────┘ └─────┘ ┴
typ └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘ ┴
295 tendsto (λ x, ∥f x∥) l (𝓝 ∥a∥) :=
id └─────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴┴
src └─────┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴┴
doc └─────┘ ┴
296 tendsto.comp continuous_norm.continuous_at h
id └──────────┘ └─────────────┘└────────────┘ ┴
src └──────────┘ └─────────────┘└────────────┘
typ └──────────┘ └─────────────┘└────────────┘ ┴
297
298 lemma continuous_nnnorm : continuous (nnnorm : α → nnreal) :=
id └────────┘ └────┘ ┴ └────┘
src └────────┘ └────┘ └────┘
typ └────────┘ └────┘ ┴ └────┘
doc └────────┘ └────┘ └────┘
299 continuous_subtype_mk _ continuous_norm
id └───────────────────┘ └─────────────┘
src └───────────────────┘ └─────────────┘
typ └───────────────────┘ └─────────────┘
300
301 lemma filter.tendsto.nnnorm {β : Type*} {l : filter β} {f : β → α} {a : α} (h : tendsto f l (𝓝 a)) :
id └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └────┘ └─────┘ ┴
typ └────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘ ┴
302 tendsto (λ x, nnnorm (f x)) l (𝓝 (nnnorm a)) :=
id └─────┘ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴
src └─────┘ └────┘ ┴ └────┘
typ └─────┘ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴
doc └─────┘ └────┘ ┴ └────┘
303 tendsto.comp continuous_nnnorm.continuous_at h
id └──────────┘ └───────────────┘└────────────┘ ┴
src └──────────┘ └───────────────┘└────────────┘
typ └──────────┘ └───────────────┘└────────────┘ ┴
304
305 /-- If `∥y∥→∞`, then we can assume `y≠x` for any fixed `x`. -/
306 lemma ne_mem_of_tendsto_norm_at_top {l : filter γ} {f : γ → α}
id └────┘ ┴ ┴ ┴
src └────┘
typ └────┘ ┴ ┴ ┴
307 (h : tendsto (λ y, ∥f y∥) l at_top) (x : α) :
id └─────┘ ┴ ┴┴ ┴┴ ┴ └────┘ ┴
src └─────┘ ┴ ┴ └────┘
typ └─────┘ ┴ ┴┴ ┴┴ ┴ └────┘ ┴
doc └─────┘ └────┘
308 ∀ᶠ y in l, f y ≠ x :=
id └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴
src └┘ └┘ ┴ ┴
typ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴
doc └┘ └┘ ┴
309 begin
st └─────
310 have : ∀ᶠ y in l, 1 + ∥x∥ ≤ ∥f y∥ := h (mem_at_top (1 + ∥x∥)),
id └┘ └┘ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴ └────────┘ ┴
src └─────┘└┘└─┘└┘┴ ┴└─┘┴┴┴ ┴┴┴┴ ┴ └──┘ ┴ └────────┘┴ └┘ ┴ └┘
typ └─────┘└┘└─┘└┘┴┴┴└─┘┴┴┴┴┴┴┴┴ ┴┴ └──┘┴┴ └────────┘┴ └┘ ┴ ┴ └┘
doc └─────┘└┘└─┘└┘┴ ┴└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘
txt └─────┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘
par └─────┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘
pid └───┘└┘ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘
st ──────────────────────────────────────────────────────────────┘└─
311 apply mem_sets_of_superset this,
id └──────────────────┘ └──┘
src └────┘└──────────────────┘┴
typ └────┘└──────────────────┘┴└──┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────┘└─
312 assume y hy hxy,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └─────────────┘
st ────────────────┘└─
313 subst x,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────┘└─
314 simp at hy,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ───────────┘└─
315 exact not_le_of_lt zero_lt_one hy
id └──────────┘ └─────────┘ └┘
src └────┘└──────────┘┴└─────────┘┴ ┴
typ └────┘└──────────┘┴└─────────┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────┘
316 end
st └─┘
317
318 /-- A normed group is a uniform additive group, i.e., addition and subtraction are uniformly
319 continuous. -/
320 @[priority 100] -- see Note [lower instance priority]
321 instance normed_uniform_group : uniform_add_group α :=
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
doc └───────────────┘
322 begin
st └─────
323 refine ⟨metric.uniform_continuous_iff.2 $ assume ε hε, ⟨ε / 2, half_pos hε, assume a b h, _⟩⟩,
id └───────────────────────────┘ ┴ └──────┘
src └─────┘ └───────────────────────────┘└─┘ ┴ └─────┘ ┴┴└──┘└──────┘┴ └┘ └─────────┘
typ └─────┘ └───────────────────────────┘└─┘ ┴ └─────┘ ┴┴└──┘└──────┘┴ └┘ └─────────┘
doc └─────┘ └─┘ ┴ └─────┘ ┴ └──┘ ┴ └┘ └─────────┘
txt └─────┘ └─┘ ┴ └─────┘ ┴ └──┘ ┴ └┘ └─────────┘
par └─────┘ └─┘ ┴ └─────┘ ┴ └──┘ ┴ └┘ └─────────┘
pid ┴ └─┘ ┴ └─────┘ ┴ └──┘ ┴ └┘ └─────────┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
324 rw [prod.dist_eq, max_lt_iff, dist_eq_norm, dist_eq_norm] at h,
id └──────────┘ └────────┘ └──────────┘ └──────────┘
src └──┘└──────────┘└┘└────────┘└┘└──────────┘└┘└──────────┘└────┘
typ └──┘└──────────┘└┘└────────┘└┘└──────────┘└┘└──────────┘└────┘
doc └──┘ └┘ └┘ └┘ └────┘
txt └──┘ └┘ └┘ └┘ └────┘
par └──┘ └┘ └┘ └┘ └────┘
pid └┘ └┘ └┘ └┘ ┴└───┘
st ─────────────────┘└──────────┘└────────────┘└────────────┘┴└───┘└─
325 calc dist (a.1 - a.2) (b.1 - b.2) = ∥(a.1 - b.1) - (a.2 - b.2)∥ : by simp [dist_eq_norm]
id └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘
src └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘└──────────┘└─
typ └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└──────────┘└─
doc └──┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st ──────────────────────────────────────────────────────────────────────┘└────────────────────
326 ... ≤ ∥a.1 - b.1∥ + ∥a.2 - b.2∥ : norm_sub_le _ _
id ┴ ┴ └─────────┘
src ───┘ ┴ ┴ └─────────┘
typ ───┘ ┴ ┴ └─────────┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─────────────────────────────────────────────────
327 ... < ε / 2 + ε / 2 : add_lt_add h.1 h.2
id ┴ └────────┘ ┴ ┴┴
src ┴ └────────┘ ┴ ┴
typ ┴ └────────┘ ┴ ┴┴
st ─────────────────────────────────────────────
328 ... = ε : add_halves _
id ┴ └────────┘
src └────────┘
typ ┴ └────────┘
st ─────────────────────────┘└
329 end
st ──┘
330
331 @[priority 100] -- see Note [lower instance priority]
332 instance normed_top_monoid : topological_add_monoid α := by apply_instance -- short-circuit type class inference
id └────────────────────┘ ┴
src └────────────────────┘ └───────────────────────────────────────────────────┘
typ └────────────────────┘ ┴ └───────────────────────────────────────────────────┘
doc └────────────────────┘ └───────────────────────────────────────────────────┘
txt └───────────────────────────────────────────────────┘
par └───────────────────────────────────────────────────┘
pid └─────────────────────────────────────┘
st └────────────────────────────────────────────────────┘
333 @[priority 100] -- see Note [lower instance priority]
334 instance normed_top_group : topological_add_group α := by apply_instance -- short-circuit type class inference
id └───────────────────┘ ┴
src └───────────────────┘ └────────────────────────────────────────────────────
typ └───────────────────┘ ┴ └────────────────────────────────────────────────────
doc └───────────────────┘ └────────────────────────────────────────────────────
txt └────────────────────────────────────────────────────
par └────────────────────────────────────────────────────
pid └──────────────────────────────────────
st └─────────────────────────────────────────────────────
335
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
336 end normed_group
337
338 section normed_ring
339
340 section prio
341 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
342 /-- A normed ring is a ring endowed with a norm which satisfies the inequality `∥x y∥ ≤ ∥x∥ ∥y∥`. -/
343 class normed_ring (α : Type*) extends has_norm α, ring α, metric_space α :=
id └───┘ └──────┘ ┴ └──┘ ┴ └──────────┘ ┴
src └──────┘ └──┘ └──────────┘
typ └───┘ └──────┘ ┴ └──┘ ┴ └──────────┘ ┴
doc └──────┘ └──────────┘
344 (dist_eq : ∀ x y, dist x y = norm (x - y))
id ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
345 (norm_mul : ∀ a b, norm (a * b) ≤ norm a * norm b)
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
346 end prio
347
348 @[priority 100] -- see Note [lower instance priority]
349 instance normed_ring.to_normed_group [β : normed_ring α] : normed_group α := { ..β }
id └─────────┘ ┴ └──────────┘ ┴ ┴
src └─────────┘ └──────────┘
typ └─────────┘ ┴ └──────────┘ ┴ ┴
doc └─────────┘ └──────────┘
350
351 lemma norm_mul_le {α : Type*} [normed_ring α] (a b : α) : (∥a*b∥) ≤ (∥a∥) * (∥b∥) :=
id └─────────┘ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴ ┴┴┴
doc └─────────┘
352 normed_ring.norm_mul _ _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
353
354 lemma norm_pow_le {α : Type*} [normed_ring α] (a : α) : ∀ {n : ℕ}, 0 < n → ∥a^n∥ ≤ ∥a∥^n
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴┴┴
src └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴┴┴
doc └─────────┘
355 | 1 h := by simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
356 | (n+2) h :=
id ┴┴
src ┴
typ ┴┴
357 le_trans (norm_mul_le a (a^(n+1)))
id └──────┘ └─────────┘ ┴ ┴┴ ┴
src └──────┘ └─────────┘ ┴ ┴
typ └──────┘ └─────────┘ ┴ ┴┴ ┴
358 (mul_le_mul (le_refl _)
id └────────┘ └─────┘
src └────────┘ └─────┘
typ └────────┘ └─────┘
359 (norm_pow_le (nat.succ_pos _)) (norm_nonneg _) (norm_nonneg _))
id └─────────┘ └──────────┘ └─────────┘ └─────────┘
src └──────────┘ └─────────┘ └─────────┘
typ └─────────┘ └──────────┘ └─────────┘ └─────────┘
360
361 /-- Normed ring structure on the product of two normed rings, using the sup norm. -/
362 instance prod.normed_ring [normed_ring α] [normed_ring β] : normed_ring (α × β) :=
id └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴ ┴
src └─────────┘ └─────────┘ └─────────┘ ┴
typ └─────────┘ ┴ └─────────┘ ┴ └─────────┘ ┴ ┴ ┴
doc └─────────┘ └─────────┘ └─────────┘
363 { norm_mul := assume x y,
id ┴ ┴
typ ┴ ┴
364 calc
365 ∥x * y∥ = ∥(x.1*y.1, x.2*y.2)∥ : rfl
id ┴┴ ┴ ┴┴ ┴┴┴┴ ┴┴┴ ┴┴ ┴┴┴ ┴ └─┘
src ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴┴ ┴ ┴┴ ┴┴┴┴ ┴┴┴ ┴┴ ┴┴┴ ┴ └─┘
366 ... = (max ∥x.1*y.1∥ ∥x.2*y.2∥) : rfl
id └─┘ ┴┴┴ ┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴ └─┘
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ └─┘ ┴┴┴ ┴┴┴ ┴ ┴┴┴ ┴┴┴ ┴ └─┘
367 ... ≤ (max (∥x.1∥*∥y.1∥) (∥x.2∥*∥y.2∥)) :
id └─┘ ┴┴┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴┴┴┴┴ ┴
src └─┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴
typ └─┘ ┴┴┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴┴┴┴┴ ┴
368 max_le_max (norm_mul_le (x.1) (y.1)) (norm_mul_le (x.2) (y.2))
id └────────┘ └─────────┘ ┴┴ ┴┴ └─────────┘ ┴┴ ┴┴
src └────────┘ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴
typ └────────┘ └─────────┘ ┴┴ ┴┴ └─────────┘ ┴┴ ┴┴
369 ... = (max (∥x.1∥*∥y.1∥) (∥y.2∥*∥x.2∥)) : by simp[mul_comm]
id └─┘ ┴┴┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴┴┴┴┴ ┴ └──────┘
src └─┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ └───┘└──────┘└─
typ └─┘ ┴┴┴ ┴┴┴┴┴ ┴ ┴┴┴ ┴┴┴┴┴ ┴ └───┘└──────┘└─
doc └───┘ └─
txt └───┘ └─
par └───┘ └─
pid ┴ ┴└
st └───────────────
370 ... ≤ (max (∥x.1∥) (∥x.2∥)) * (max (∥y.2∥) (∥y.1∥)) : by { apply max_mul_mul_le_max_mul_max; simp [norm_nonneg] }
id └─┘ ┴┴┴ ┴ ┴┴┴ ┴ ┴ └─┘ ┴┴┴ ┴ ┴┴┴ ┴ └────────────────────────┘ └─────────┘
src ───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘└────────────────────────┘ └────┘└─────────┘└┘
typ ───────┘ └─┘ ┴┴┴ ┴ ┴┴┴ ┴ ┴ └─┘ ┴┴┴ ┴ ┴┴┴ ┴ └────┘└────────────────────────┘ └────┘└─────────┘└┘
doc ───────┘ └────┘ └────┘ └┘
txt ───────┘ └────┘ └────┘ └┘
par ───────┘ └────┘ └────┘ └┘
pid ───────┘ ┴ ┴┴ ┴┴
st ───────┘ └──────────────────────────────────────────────────────┘└┘
371 ... = (max (∥x.1∥) (∥x.2∥)) * (max (∥y.1∥) (∥y.2∥)) : by simp[max_comm]
id └─┘ ┴┴┴ ┴ ┴┴┴ ┴ ┴ └─┘ ┴┴┴ ┴ ┴┴┴ ┴ └──────┘
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘└──────┘└─
typ └─┘ ┴┴┴ ┴ ┴┴┴ ┴ ┴ └─┘ ┴┴┴ ┴ ┴┴┴ ┴ └───┘└──────┘└─
doc └───┘ └─
txt └───┘ └─
par └───┘ └─
pid ┴ ┴└
st └───────────────
372 ... = (∥x∥*∥y∥) : rfl,
id ┴┴┴┴┴┴┴ └─┘
src ───────┘ ┴ ┴┴┴ ┴ └─┘
typ ───────┘ ┴┴┴┴┴┴┴ └─┘
doc ───────┘
txt ───────┘
par ───────┘
pid ───────┘
st ───────┘
373 ..prod.normed_group }
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
374 end normed_ring
375
376 @[priority 100] -- see Note [lower instance priority]
377 instance normed_ring_top_monoid [normed_ring α] : topological_monoid α :=
id └─────────┘ ┴ └────────────────┘ ┴
src └─────────┘ └────────────────┘
typ └─────────┘ ┴ └────────────────┘ ┴
doc └─────────┘ └────────────────┘
378 ⟨ continuous_iff_continuous_at.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
id └──────────────────────────┘┴ ┴ └───────────────────────────┘┴
src └──────────────────────────┘┴ └───────────────────────────┘┴
typ └──────────────────────────┘┴ ┴ └───────────────────────────┘┴
379 have ∀ e : α × α, e.fst * e.snd - x.fst * x.snd =
id ┴ ┴ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴
src ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴
380 e.fst * e.snd - e.fst * x.snd + (e.fst * x.snd - x.fst * x.snd), by intro; rw sub_add_sub_cancel,
id ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ └────────────────┘
src └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ └───┘ └─┘└────────────────┘
typ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴└──┘ └───┘ └─┘└────────────────┘
doc └───┘ └─┘
txt └───┘ └─┘
par └───┘ └─┘
pid ┴
st └─────────┘└────────────────┘
381 begin
st └─────
382 apply squeeze_zero,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘└─
383 { intro, apply norm_nonneg },
id └─────────┘
src └───┘ └────┘└─────────┘┴
typ └───┘ └────┘└─────────┘┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid ┴ ┴
st ───────┘└───┘└──────────────────┘└┘└
384 { simp only [this], intro, apply norm_add_le },
id └──┘ └─────────┘
src └─────────┘ ┴ └───┘ └────┘└─────────┘┴
typ └─────────┘└──┘┴ └───┘ └────┘└─────────┘┴
doc └─────────┘ ┴ └───┘ └────┘└─────────┘┴
txt └─────────┘ ┴ └───┘ └────┘ ┴
par └─────────┘ ┴ └───┘ └────┘ ┴
pid ┴└──┘└┘ ┴ ┴ ┴
st ───────┘└──────────────┘└─────┘└──────────────────┘└┘└
385 { rw ←zero_add (0 : ℝ), apply tendsto.add,
id └──────┘ └─────────┘
src └──┘└──────┘┴ └──┘ ┴ └────┘└─────────┘
typ └──┘└──────┘┴ └──┘ ┴ └────┘└─────────┘
doc └──┘ ┴ └──┘ ┴ └────┘
txt └──┘ ┴ └──┘ ┴ └────┘
par └──┘ ┴ └──┘ ┴ └────┘
pid └┘ ┴ └──┘ ┴ ┴
st ───────────────────────────┘└─────────────────┘└─
386 { apply squeeze_zero,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────┘└────────────────┘└─
387 { intro, apply norm_nonneg },
id └─────────┘
src └───┘ └────┘└─────────┘┴
typ └───┘ └────┘└─────────┘┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid ┴ ┴
st ───────────┘└───┘└──────────────────┘└┘└
388 { intro t, show ∥t.fst * t.snd - t.fst * x.snd∥ ≤ ∥t.fst∥ * ∥t.snd - x.snd∥,
id ┴ ┴ ┴ ┴ ┴ └───┘ └───┘ └───┘
src └─────┘ └───┘┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴┴┴ └───┘ ┴ ┴ └───┘┴ ┴└───┘
typ └─────┘ └───┘┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴┴┴┴ └───┘ ┴ ┴ └───┘┴ ┴└───┘
doc └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────┘└─────┘└────────────────────────────────────────────────────────────────┘└─
389 rw ←mul_sub, apply norm_mul_le },
id └─────┘ └─────────┘
src └──┘└─────┘ └────┘└─────────┘┴
typ └──┘└─────┘ └────┘└─────────┘┴
doc └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid └┘ ┴ ┴
st ──────────────────────┘└──────────────────┘└┘└
390 { rw ←mul_zero (∥x.fst∥), apply tendsto.mul,
id └──────┘ └───┘ └─────────┘
src └──┘└──────┘┴ └───┘ ┴ └────┘└─────────┘
typ └──┘└──────┘┴ └───┘ ┴ └────┘└─────────┘
doc └──┘ ┴ ┴ └────┘
txt └──┘ ┴ ┴ └────┘
par └──┘ ┴ ┴ └────┘
pid └┘ ┴ ┴ ┴
st ─────────────────────────────────┘└─────────────────┘└─
391 { apply continuous_iff_continuous_at.1,
id └──────────────────────────┘
src └────┘└──────────────────────────┘└┘
typ └────┘└──────────────────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────┘└──────────────────────────────────┘└─
392 apply continuous_norm.comp continuous_fst },
id └──────────────────┘ └────────────┘
src └────┘└──────────────────┘┴└────────────┘┴
typ └────┘└──────────────────┘┴└────────────┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└┘└
393 { apply tendsto_iff_norm_tendsto_zero.1,
id └───────────────────────────┘
src └────┘└───────────────────────────┘└┘
typ └────┘└───────────────────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ──────────────────────────────────────────────────┘└─
394 apply continuous_iff_continuous_at.1,
id └──────────────────────────┘
src └────┘└──────────────────────────┘└┘
typ └────┘└──────────────────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────────────────────────────────────┘└─
395 apply continuous_snd }}},
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────┘└──┘└
396 { apply squeeze_zero,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────┘└─
397 { intro, apply norm_nonneg },
id └─────────┘
src └───┘ └────┘└─────────┘┴
typ └───┘ └────┘└─────────┘┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid ┴ ┴
st ───────────┘└───┘└──────────────────┘└┘└
398 { intro t, show ∥t.fst * x.snd - x.fst * x.snd∥ ≤ ∥t.fst - x.fst∥ * ∥x.snd∥,
id └───┘ └───┘ └───┘
src └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘┴ ┴└───┘ ┴ ┴ └───┘
typ └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘┴ ┴└───┘ ┴ ┴ └───┘
doc └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────┘└─────┘└────────────────────────────────────────────────────────────────┘└─
399 rw ←sub_mul, apply norm_mul_le },
id └─────┘ └─────────┘
src └──┘└─────┘ └────┘└─────────┘┴
typ └──┘└─────┘ └────┘└─────────┘┴
doc └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid └┘ ┴ ┴
st ──────────────────────┘└──────────────────┘└┘└
400 { rw ←zero_mul (∥x.snd∥), apply tendsto.mul,
id └──────┘ └───┘ └─────────┘
src └──┘└──────┘┴ └───┘ ┴ └────┘└─────────┘
typ └──┘└──────┘┴ └───┘ ┴ └────┘└─────────┘
doc └──┘ ┴ ┴ └────┘
txt └──┘ ┴ ┴ └────┘
par └──┘ ┴ ┴ └────┘
pid └┘ ┴ ┴ ┴
st ─────────────────────────────────┘└─────────────────┘└─
401 { apply tendsto_iff_norm_tendsto_zero.1,
id └───────────────────────────┘
src └────┘└───────────────────────────┘└┘
typ └────┘└───────────────────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────┘└───────────────────────────────────┘└─
402 apply continuous_iff_continuous_at.1,
id └──────────────────────────┘
src └────┘└──────────────────────────┘└┘
typ └────┘└──────────────────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────────────────────────────────────┘└─
403 apply continuous_fst },
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────┘└┘└
404 { apply tendsto_const_nhds }}}}
id └────────────────┘
src └────┘└────────────────┘┴
typ └────┘└────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────────────┘└────
405 end ⟩
st ──────┘
406
407 /-- A normed ring is a topological ring. -/
408 @[priority 100] -- see Note [lower instance priority]
409 instance normed_top_ring [normed_ring α] : topological_ring α :=
id └─────────┘ ┴ └──────────────┘ ┴
src └─────────┘ └──────────────┘
typ └─────────┘ ┴ └──────────────┘ ┴
doc └─────────┘ └──────────────┘
410 ⟨ continuous_iff_continuous_at.2 $ λ x, tendsto_iff_norm_tendsto_zero.2 $
id └──────────────────────────┘┴ ┴ └───────────────────────────┘┴
src └──────────────────────────┘┴ └───────────────────────────┘┴
typ └──────────────────────────┘┴ ┴ └───────────────────────────┘┴
411 have ∀ e : α, -e - -x = -(e - x), by intro; simp,
id ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──┘
typ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──┘
doc └───┘ └──┘
txt └───┘ └──┘
par └───┘ └──┘
st └──────────┘
412 by simp only [this, norm_neg]; apply lim_norm ⟩
id └──┘ └──────┘ └──────┘
src └─────────┘ └┘└──────┘┴ └────┘└──────┘┴
typ └─────────┘└──┘└┘└──────┘┴ └────┘└──────┘┴
doc └─────────┘ └┘ ┴ └────┘ ┴
txt └─────────┘ └┘ ┴ └────┘ ┴
par └─────────┘ └┘ ┴ └────┘ ┴
pid ┴└──┘└┘ └┘ ┴ ┴ ┴
st └──────────────────────────────────────────┘
413
414 section prio
415 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
416 /-- A normed field is a field with a norm satisfying ∥x y∥ = ∥x∥ ∥y∥. -/
417 class normed_field (α : Type*) extends has_norm α, discrete_field α, metric_space α :=
id └───┘ └──────┘ ┴ └────────────┘ ┴ └──────────┘ ┴
src └──────┘ └────────────┘ └──────────┘
typ └───┘ └──────┘ ┴ └────────────┘ ┴ └──────────┘ ┴
doc └──────┘ └──────────┘
418 (dist_eq : ∀ x y, dist x y = norm (x - y))
id ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
419 (norm_mul' : ∀ a b, norm (a * b) = norm a * norm b)
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src ┴ ┴ ┴
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
420
421 /-- A nondiscrete normed field is a normed field in which there is an element of norm different from
422 `0` and `1`. This makes it possible to bring any element arbitrarily close to `0` by multiplication
423 by the powers of any element, and thus to relate algebra and topology. -/
424 class nondiscrete_normed_field (α : Type*) extends normed_field α :=
id └───┘ └──────────┘ ┴
src └──────────┘
typ └───┘ └──────────┘ ┴
doc └──────────┘
425 (non_trivial : ∃x:α, 1<∥x∥)
id ┴ ┴┴ ┴┴┴┴
src ┴ ┴ ┴┴ ┴
typ ┴ ┴┴ ┴┴┴┴
426 end prio
427
428 @[priority 100] -- see Note [lower instance priority]
429 instance normed_field.to_normed_ring [i : normed_field α] : normed_ring α :=
id └──────────┘ ┴ └─────────┘ ┴
src └──────────┘ └─────────┘
typ └──────────┘ ┴ └─────────┘ ┴
doc └──────────┘ └─────────┘
430 { norm_mul := by finish [i.norm_mul'], ..i }
id ┴
src └──────┘ ┴
typ └──────┘└─────────┘┴ ┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid └┘ ┴
st └───────────────────┘
431
432 namespace normed_field
433 @[simp] lemma norm_one {α : Type*} [normed_field α] : ∥(1 : α)∥ = 1 :=
id └──────────┘ ┴ ┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └──────────┘
434 have ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α)∥ * 1, by calc
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └──┘
st └─────
435 ∥(1 : α)∥ * ∥(1 : α)∥ = ∥(1 : α) * (1 : α)∥ : by rw normed_field.norm_mul'
id ┴ ┴ ┴ └────────────────────┘
src ┴ ┴ ┴ └─┘└────────────────────┘└
typ ┴ ┴ ┴ └─┘└────────────────────┘└
doc └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st ────────────────────────────────────────────────┘└──────────────────────────
436 ... = ∥(1 : α)∥ * 1 : by simp,
id ┴
src ─────────────────┘ └──┘
typ ─────────────────┘ ┴ └──┘
doc ─────────────────┘ └──┘
txt ─────────────────┘ └──┘
par ─────────────────┘ └──┘
pid ─────────────────┘
st ─────────────────┘└──────────────────────┘└───┘
437 eq_of_mul_eq_mul_left (ne_of_gt ((norm_pos_iff _).2 (by simp))) this
id └───────────────────┘ └──────┘ └──────────┘ ┴ └──┘
src └───────────────────┘ └──────┘ └──────────┘ ┴ └──┘
typ └───────────────────┘ └──────┘ └──────────┘ ┴ └──┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
438
439 @[simp] lemma norm_mul [normed_field α] (a b : α) : ∥a * b∥ = ∥a∥ * ∥b∥ :=
id └──────────┘ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
doc └──┘ └──────────┘
440 normed_field.norm_mul' a b
id └────────────────────┘ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴
441
442 instance normed_field.is_monoid_hom_norm [normed_field α] : is_monoid_hom (norm : α → ℝ) :=
id └──────────┘ ┴ └───────────┘ └──┘ ┴ ┴
src └──────────┘ └───────────┘ └──┘ ┴
typ └──────────┘ ┴ └───────────┘ └──┘ ┴ ┴
doc └──────────┘ └───────────┘
443 { map_one := norm_one, map_mul := norm_mul }
id └──────┘ └──────┘
src └──────┘ └──────┘
typ └──────┘ └──────┘
444
445 @[simp] lemma norm_pow [normed_field α] (a : α) : ∀ (n : ℕ), ∥a^n∥ = ∥a∥^n :=
id └──────────┘ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴┴┴
src └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
typ └──────────┘ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴┴┴
doc └──┘ └──────────┘
446 is_monoid_hom.map_pow norm a
id └───────────────────┘ └──┘ ┴
src └───────────────────┘ └──┘
typ └───────────────────┘ └──┘ ┴
447
448 @[simp] lemma norm_prod {β : Type*} [normed_field α] (s : finset β) (f : β → α) :
id └──────────┘ ┴ └────┘ ┴ ┴ ┴
src └──────────┘ └────┘
typ └──────────┘ ┴ └────┘ ┴ ┴ ┴
doc └──┘ └──────────┘ └────┘
449 ∥s.prod f∥ = s.prod (λb, ∥f b∥) :=
id ┴┴└───┘ ┴┴ ┴ ┴└───┘ ┴ ┴┴ ┴┴
src ┴ └───┘ ┴ ┴ └───┘ ┴ ┴
typ ┴┴└───┘ ┴┴ ┴ ┴└───┘ ┴ ┴┴ ┴┴
doc └───┘ └───┘
450 eq.symm (s.prod_hom norm)
id └─────┘ ┴└───────┘ └──┘
src └─────┘ └───────┘ └──┘
typ └─────┘ ┴└───────┘ └──┘
451
452 @[simp] lemma norm_div {α : Type*} [normed_field α] (a b : α) : ∥a/b∥ = ∥a∥/∥b∥ :=
id └──────────┘ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴┴┴┴┴
src └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴
typ └──────────┘ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴┴┴┴┴
doc └──┘ └──────────┘
453 if hb : b = 0 then by simp [hb] else
id └┘ ┴ ┴ └┘
src └┘ ┴ └────┘ └┘
typ └┘ ┴ ┴ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └─────────┘
454 begin
st └─────
455 apply eq_div_of_mul_eq,
id └──────────────┘
src └────┘└──────────────┘
typ └────┘└──────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────┘└─
456 { apply ne_of_gt, apply (norm_pos_iff _).mpr hb },
id └──────┘ └──────────┘ └┘
src └────┘└──────┘ └────┘ └──────────┘└──────┘ ┴
typ └────┘└──────┘ └────┘ └──────────┘└──────┘└┘┴
doc └────┘ └────┘ └──────┘ ┴
txt └────┘ └────┘ └──────┘ ┴
par └────┘ └────┘ └──────┘ ┴
pid ┴ ┴ └──────┘ ┴
st ───┘└────────────┘└──────────────────────────────┘└┘└
457 { rw [←normed_field.norm_mul, div_mul_cancel _ hb] }
id └───────────────────┘ └────────────┘ └┘
src └───┘└───────────────────┘└┘└────────────┘└─┘ └┘
typ └───┘└───────────────────┘└┘└────────────┘└─┘└┘└┘
doc └───┘ └┘ └─┘ └┘
txt └───┘ └┘ └─┘ └┘
par └───┘ └┘ └─┘ └┘
pid └─┘ └┘ └─┘ ┴┴
st ─────────────────────────────┘└───────────────────┘┴┴└─
458 end
id └─┘
src └─┘
typ └─┘
st ──┘
459
460 @[simp] lemma norm_inv {α : Type*} [normed_field α] (a : α) : ∥a⁻¹∥ = ∥a∥⁻¹ :=
id └──────────┘ ┴ ┴ ┴┴└┘┴ ┴ ┴┴┴└┘
src └──────────┘ ┴ └┘┴ ┴ ┴ ┴└┘
typ └──────────┘ ┴ ┴ ┴┴└┘┴ ┴ ┴┴┴└┘
doc └──┘ └──────────┘
461 by simp only [inv_eq_one_div, norm_div, norm_one]
id └────────────┘ └──────┘ └──────┘
src └─────────┘└────────────┘└┘└──────┘└┘└──────┘└─
typ └─────────┘└────────────┘└┘└──────┘└┘└──────┘└─
doc └─────────┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────
462
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
463 @[simp] lemma norm_fpow {α : Type*} [normed_field α] (a : α) : ∀n : ℤ,
id └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴
doc └──┘ └──────────┘
464 ∥a^n∥ = ∥a∥^n
id ┴┴┴┴┴ ┴ ┴┴┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴┴
typ ┴┴┴┴┴ ┴ ┴┴┴┴┴
465 | (n : ℕ) := norm_pow a n
id ┴ ┴ └──────┘ ┴
src ┴ └──────┘
typ ┴ ┴ └──────┘ ┴
466 | -[1+ n] := by simp [fpow_neg_succ_of_nat]
id └──┘ ┴ └──────────────────┘
src └──┘ ┴ └────┘└──────────────────┘└─
typ └──┘ ┴ └────┘└──────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────────────
467
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
468 lemma exists_one_lt_norm (α : Type*) [i : nondiscrete_normed_field α] : ∃x : α, 1 < ∥x∥ :=
id └──────────────────────┘ ┴ ┴ ┴┴ ┴ ┴┴┴
src └──────────────────────┘ ┴ ┴ ┴ ┴ ┴
typ └──────────────────────┘ ┴ ┴ ┴┴ ┴ ┴┴┴
doc └──────────────────────┘
469 i.non_trivial
id ┴└──────────┘
src └──────────┘
typ ┴└──────────┘
470
471 lemma exists_norm_lt_one (α : Type*) [nondiscrete_normed_field α] : ∃x : α, 0 < ∥x∥ ∧ ∥x∥ < 1 :=
id └──────────────────────┘ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴
src └──────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────────────────────┘ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴
doc └──────────────────────┘
472 begin
st └─────
473 rcases exists_one_lt_norm α with ⟨y, hy⟩,
id └────────────────┘ ┴
src └─────┘└────────────────┘┴ └───────────┘
typ └─────┘└────────────────┘┴┴└───────────┘
doc └─────┘ ┴ └───────────┘
txt └─────┘ ┴ └───────────┘
par └─────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st ─────────────────────────────────────────┘└─
474 refine ⟨y⁻¹, _, _⟩,
id ┴└┘
src └─────┘ └┘└─────┘
typ └─────┘ ┴└┘└─────┘
doc └─────┘ └─────┘
txt └─────┘ └─────┘
par └─────┘ └─────┘
pid ┴ └─────┘
st ───────────────────┘└─
475 { simp only [inv_eq_zero, ne.def, norm_pos_iff],
id └─────────┘ └────┘ └──────────┘
src └─────────┘└─────────┘└┘└────┘└┘└──────────┘┴
typ └─────────┘└─────────┘└┘└────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ───┘└───────────────────────────────────────────┘└─
476 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
477 rw ← norm_eq_zero at h,
id └──────────┘
src └───┘└──────────┘└───┘
typ └───┘└──────────┘└───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └─┘ └───┘
st ─────────────────────────┘└─
478 rw h at hy,
id ┴
src └─┘ └────┘
typ └─┘┴└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ─────────────┘└─
479 exact lt_irrefl _ (lt_trans zero_lt_one hy) },
id └───────┘ └──────┘ └─────────┘ └┘
src └────┘└───────┘└─┘ └──────┘┴└─────────┘┴ └┘
typ └────┘└───────┘└─┘ └──────┘┴└─────────┘┴└┘└┘
doc └────┘ └─┘ ┴ ┴ └┘
txt └────┘ └─┘ ┴ ┴ └┘
par └────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ───────────────────────────────────────────────┘└┘└
480 { simp [inv_lt_one hy] }
id └────────┘ └┘
src └────┘└────────┘┴ └┘
typ └────┘└────────┘┴└┘└┘
doc └────┘ ┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴┴ ┴ ┴┴
st ────────────────────────┘└─
481 end
st ──┘
482
483 lemma exists_lt_norm (α : Type*) [nondiscrete_normed_field α]
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
484 (r : ℝ) : ∃ x : α, r < ∥x∥ :=
id ┴ ┴ ┴┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴┴┴
485 let ⟨w, hw⟩ := exists_one_lt_norm α in
id └─┘ ┴ └┘ └────────────────┘ ┴
src └────────────────┘
typ └─┘ ┴ └┘ └────────────────┘ ┴
486 let ⟨n, hn⟩ := pow_unbounded_of_one_lt r hw in
id └─┘ ┴ └─────────────────────┘ ┴
src └─────────────────────┘
typ └─┘ ┴ └─────────────────────┘ ┴
487 ⟨w^n, by rwa norm_pow⟩
id ┴ └──────┘
src ┴ └──┘└──────┘
typ ┴ └──┘└──────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └───────────┘
488
489 lemma exists_norm_lt (α : Type*) [nondiscrete_normed_field α]
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
490 {r : ℝ} (hr : 0 < r) : ∃ x : α, 0 < ∥x∥ ∧ ∥x∥ < r :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴
491 let ⟨w, hw⟩ := exists_one_lt_norm α in
id └─┘ ┴ └┘ └────────────────┘ ┴
src └────────────────┘
typ └─┘ ┴ └┘ └────────────────┘ ┴
492 let ⟨n, hle, hlt⟩ := exists_int_pow_near' hr hw in
id └─┘ ┴ └──────────────────┘ └┘
src └──────────────────┘
typ └─┘ ┴ └──────────────────┘ └┘
doc └──────────────────┘
493 ⟨w^n, by { rw norm_fpow; exact fpow_pos_of_pos (lt_trans zero_lt_one hw) _},
id ┴ └───────┘ └─────────────┘ └──────┘ └─────────┘ └┘
src ┴ └─┘└───────┘ └────┘└─────────────┘┴ └──────┘┴└─────────┘┴ └─┘
typ ┴ └─┘└───────┘ └────┘└─────────────┘┴ └──────┘┴└─────────┘┴└┘└─┘
doc └─┘ └────┘ ┴ ┴ ┴ └─┘
txt └─┘ └────┘ ┴ ┴ ┴ └─┘
par └─┘ └────┘ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ ┴ └─┘
st └────────────────────────────────────────────────────────────────┘└┘
494 by rwa norm_fpow⟩
id └───────┘
src └──┘└───────┘
typ └──┘└───────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └────────────┘
495
496 lemma tendsto_inv [normed_field α] {r : α} (r0 : r ≠ 0) : tendsto (λq, q⁻¹) (𝓝 r) (𝓝 r⁻¹) :=
id └──────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘
src └──────────┘ ┴ └─────┘ └┘ ┴ ┴ └┘
typ └──────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└┘ ┴ ┴ ┴ ┴└┘
doc └──────────┘ └─────┘ ┴ ┴
497 begin
st └─────
498 refine metric.tendsto_nhds.2 (λε εpos, _),
id └─────────────────┘
src └─────┘└─────────────────┘└─┘ └────────┘
typ └─────┘└─────────────────┘└─┘ └────────┘
doc └─────┘ └─┘ └────────┘
txt └─────┘ └─┘ └────────┘
par └─────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ──────────────────────────────────────────┘└─
499 let δ := min (ε/2/2 * ∥r∥^2) (∥r∥/2),
id └─┘ ┴┴ ┴ ┴ ┴┴ ┴
src └───────┘└─┘┴ ┴┴ └┘┴┴┴ ┴┴└─┘ └┘
typ └───────┘└─┘┴ ┴┴┴ └┘┴┴┴ ┴┴└─┘ ┴ └┘
doc └───────┘ ┴ ┴ └┘ ┴ └─┘ └┘
txt └───────┘ ┴ ┴ └┘ ┴ └─┘ └┘
par └───────┘ ┴ ┴ └┘ ┴ └─┘ └┘
pid └───┘┴└─┘ ┴ ┴ └┘ ┴ └─┘ └┘
st ─────────────────────────────────────┘└─
500 have norm_r_pos : 0 < ∥r∥ := (norm_pos_iff r).mpr r0,
id ┴ ┴ └──────────┘ ┴ └┘
src └──────────────────┘┴┴ └──┘ └──────────┘┴ └────┘
typ └──────────────────┘┴┴ ┴ └──┘ └──────────┘┴┴└────┘└┘
doc └──────────────────┘ ┴ └──┘ ┴ └────┘
txt └──────────────────┘ ┴ └──┘ ┴ └────┘
par └──────────────────┘ ┴ └──┘ ┴ └────┘
pid └─────────────┘└───┘ ┴ └──┘ ┴ └────┘
st ─────────────────────────────────────────────────────┘└─
501 have A : 0 < ε / 2 / 2 * ∥r∥ ^ 2 := mul_pos' (half_pos (half_pos εpos)) (pow_pos norm_r_pos 2),
id ┴ ┴ └──────┘ └──────┘ └──┘ └─────┘ └────────┘
src └─────────┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────┘└──────┘┴ ┴ └──────┘┴ └─┘ └─────┘┴ └─┘
typ └─────────┘ ┴┴┴ └─┘ └─┘ ┴ ┴ ┴ └────┘└──────┘┴ ┴ └──────┘┴└──┘└─┘ └─────┘┴└────────┘└─┘
doc └─────────┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ └─┘ ┴ └─┘
txt └─────────┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ └─┘ ┴ └─┘
par └─────────┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────┘ ┴ ┴ ┴ └─┘ ┴ └─┘
pid └────┘└───┘ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └─┘ ┴ └─┘
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
502 have δpos : 0 < δ, by simp [half_pos norm_r_pos, A],
id ┴ └──────┘ └────────┘ ┴
src └────────────┘ ┴ └────┘└──────┘┴ └┘ ┴
typ └────────────┘ ┴┴ └────┘└──────┘┴└────────┘└┘┴┴
doc └────────────┘ ┴ └────┘ ┴ └┘ ┴
txt └────────────┘ ┴ └────┘ ┴ └┘ ┴
par └────────────┘ ┴ └────┘ ┴ └┘ ┴
pid └───────┘└───┘ ┴ ┴┴ ┴ └┘ ┴
st ──────────────────┘ └─
503 refine ⟨ball r δ, ball_mem_nhds r δpos, λx hx, _⟩,
id └──┘ ┴ └───────────┘ ┴ └──┘
src └─────┘ └──┘┴ ┴ └┘└───────────┘┴ ┴ └┘ └──────┘
typ └─────┘ └──┘┴ ┴┴└┘└───────────┘┴┴┴└──┘└┘ └──────┘
doc └─────┘ └──┘┴ ┴ └┘ ┴ ┴ └┘ └──────┘
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ └──────┘
par └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ └──────┘
pid ┴ ┴ ┴ └┘ ┴ ┴ └┘ └──────┘
st ──────────────────────────────────────────────────┘└─
504 have rx : ∥r∥/2 ≤ ∥x∥ := calc
id ┴ ┴ ┴
src └────────┘ └┘┴┴ └──┘ └
typ └────────┘ ┴ └┘┴┴ ┴ └──┘ └
doc └────────┘ └┘ ┴ └──┘ └
txt └────────┘ └┘ ┴ └──┘ └
par └────────┘ └┘ ┴ └──┘ └
pid └─────┘└─┘ └┘ ┴ └──┘ └
st ────────────────────────────────
505 ∥r∥/2 = ∥r∥ - ∥r∥/2 : by ring
src ───┘ └┘ ┴ ┴ ┴ └──┘ ┴└────
typ ───┘ └┘ ┴ ┴ ┴ └──┘ ┴└────
doc ───┘ └┘ ┴ ┴ ┴ └──┘ ┴└────
txt ───┘ └┘ ┴ ┴ ┴ └──┘ ┴└────
par ───┘ └┘ ┴ ┴ ┴ └──┘ ┴└────
pid ───┘ └┘ ┴ ┴ ┴ └──┘ └─────
st ───────────────────────────┘└─────
506 ... ≤ ∥r∥ - ∥r - x∥ :
src ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └──
typ ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └──
doc ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └──
txt ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └──
par ───┘└──┘ ┴ ┴ ┴ ┴ ┴ └──
pid ───────┘ ┴ ┴ ┴ ┴ ┴ └──
st ───┘└─────────────────────
507 begin
src ───┘ └
typ ───┘ └
doc ───┘ └
txt ───┘ └
par ───┘ └
pid ───┘ └
st ───┘└─────
508 apply sub_le_sub (le_refl _),
id └────────┘ └─────┘
src ─────┘└────┘└────────┘┴ └─────┘└─┘└─
typ ─────┘└────┘└────────┘┴ └─────┘└─┘└─
doc ─────┘└────┘ ┴ └─┘└─
txt ─────┘└────┘ ┴ └─┘└─
par ─────┘└────┘ ┴ └─┘└─
pid ───────────┘ ┴ └────
st ─────────────────────────────────┘└─
509 rw ← dist_eq_norm,
id └──────────┘
src ─────┘└───┘└──────────┘└─
typ ─────┘└───┘└──────────┘└─
doc ─────┘└───┘ └─
txt ─────┘└───┘ └─
par ─────┘└───┘ └─
pid ──────────┘ └─
st ──────────────────────┘└─
510 exact le_trans (le_of_lt (mem_ball'.1 hx)) (min_le_right _ _)
id └──────┘ └──────┘ └───────┘ └┘ └──────────┘
src ─────┘└────┘└──────┘┴ └──────┘┴ └───────┘└─┘ └─┘ └──────────┘└─────
typ ─────┘└────┘└──────┘┴ └──────┘┴ └───────┘└─┘└┘└─┘ └──────────┘└─────
doc ─────┘└────┘ ┴ ┴ └─┘ └─┘ └─────
txt ─────┘└────┘ ┴ ┴ └─┘ └─┘ └─────
par ─────┘└────┘ ┴ ┴ └─┘ └─┘ └─────
pid ───────────┘ ┴ ┴ └─┘ └─┘ └─────
st ────────────────────────────────────────────────────────────────────
511 end
src ───┘└───
typ ───┘└───
doc ───┘└───
txt ───┘└───
par ───┘└───
pid ────────
st ───┘└─┘└
512 ... ≤ ∥r - (r - x)∥ : norm_sub_norm_le r (r - x)
id ┴ └──────────────┘ ┴ ┴
src ───────┘ ┴ ┴┴┴ ┴ ┴ ┴ └─┘└──────────────┘┴ ┴ ┴ ┴ └─
typ ───────┘ ┴ ┴┴┴ ┴ ┴ ┴ └─┘└──────────────┘┴ ┴ ┴┴ ┴┴└─
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────────
513 ... = ∥x∥ : by simp,
src ───────┘ ┴ └─┘ ┴└──┘
typ ───────┘ ┴ └─┘ ┴└──┘
doc ───────┘ ┴ └─┘ ┴└──┘
txt ───────┘ ┴ └─┘ ┴└──┘
par ───────┘ ┴ └─┘ ┴└──┘
pid ───────┘ ┴ └─┘ └───┘
st ─────────────────┘└───┘└─
514 have norm_x_pos : 0 < ∥x∥ := lt_of_lt_of_le (half_pos norm_r_pos) rx,
id ┴ └────────────┘ └──────┘ └────────┘ └┘
src └──────────────────┘ ┴ └──┘└────────────┘┴ └──────┘┴ └┘
typ └──────────────────┘ ┴ ┴ └──┘└────────────┘┴ └──────┘┴└────────┘└┘└┘
doc └──────────────────┘ ┴ └──┘ ┴ ┴ └┘
txt └──────────────────┘ ┴ └──┘ ┴ ┴ └┘
par └──────────────────┘ ┴ └──┘ ┴ ┴ └┘
pid └─────────────┘└───┘ ┴ └──┘ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────┘└─
515 have : x⁻¹ - r⁻¹ = (r - x) * x⁻¹ * r⁻¹,
id └┘ ┴ ┴ ┴
src └─────┘ └┘┴ ┴ ┴┴┴ ┴ ┴ └┘ ┴ ┴ ┴
typ └─────┘ └┘┴ ┴ ┴┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ───────────────────────────────────────┘
516 by rw [sub_mul, sub_mul, mul_inv_cancel ((norm_pos_iff x).mp norm_x_pos), one_mul, mul_comm,
id └─────┘ └─────┘ └────────────┘ └──────────┘ ┴ └────────┘ └─────┘ └──────┘
src └──┘└─────┘└┘└─────┘└┘└────────────┘┴ └──────────┘┴ └───┘ └─┘└─────┘└┘└──────┘└─
typ └──┘└─────┘└┘└─────┘└┘└────────────┘┴ └──────────┘┴┴└───┘└────────┘└─┘└─────┘└┘└──────┘└─
doc └──┘ └┘ └┘ ┴ ┴ └───┘ └─┘ └┘ └─
txt └──┘ └┘ └┘ ┴ ┴ └───┘ └─┘ └┘ └─
par └──┘ └┘ └┘ ┴ ┴ └───┘ └─┘ └┘ └─
pid └┘ └┘ └┘ ┴ ┴ └───┘ └─┘ └┘ └─
st └─────┘└───────┘└───────────────────────────────────────────────┘└───────┘└────────┘└─
517 ← mul_assoc, inv_mul_cancel r0, one_mul],
id └───────┘ └────────────┘ └┘ └─────┘
src ────────────┘└───────┘└┘└────────────┘┴ └┘└─────┘┴
typ ────────────┘└───────┘└┘└────────────┘┴└┘└┘└─────┘┴
doc ────────────┘ └┘ ┴ └┘ ┴
txt ────────────┘ └┘ ┴ └┘ ┴
par ────────────┘ └┘ ┴ └┘ ┴
pid ────────────┘ └┘ ┴ └┘ ┴
st ─────────────────────┘└─────────────────┘└───────┘┴└─
518 calc dist x⁻¹ r⁻¹ = ∥x⁻¹ - r⁻¹∥ : dist_eq_norm _ _
id └──┘ └──┘ ┴ ┴ └──────────┘
src └──┘ └──┘ └──────────┘
typ └──┘ └──┘ ┴ ┴ └──────────┘
doc └──┘
st ─────────────────────────────────────────────────────
519 ... ≤ ∥r-x∥ * ∥x∥⁻¹ * ∥r∥⁻¹ : by rw [this, norm_mul, norm_mul, norm_inv, norm_inv]
id └──┘ └──────┘ └──────┘ └──────┘ └──────┘
src └──┘ └┘└──────┘└┘└──────┘└┘└──────┘└┘└──────┘└─
typ └──┘└──┘└┘└──────┘└┘└──────┘└┘└──────┘└┘└──────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ ┴└
st ─────────────────────────────────┘└───────┘└────────┘└────────┘└────────┘└────────┘┴└
520 ... ≤ (ε/2/2 * ∥r∥^2) * (2 * ∥r∥⁻¹) * (∥r∥⁻¹) : begin
id ┴
src ─┘
typ ─┘ ┴
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└──────────────────────────────────────────────┘└─────
521 apply_rules [mul_le_mul, inv_nonneg.2, le_of_lt A, norm_nonneg, inv_nonneg.2, mul_nonneg,
id └────────┘ └────────┘ └──────┘ ┴ └─────────┘ └────────┘ └────────┘
src └───────────┘└────────┘└┘└────────┘└──┘└──────┘┴ └┘└─────────┘└┘└────────┘└──┘└────────┘└─
typ └───────────┘└────────┘└┘└────────┘└──┘└──────┘┴┴└┘└─────────┘└┘└────────┘└──┘└────────┘└─
doc └───────────┘ └┘ └──┘ ┴ └┘ └┘ └──┘ └─
txt └───────────┘ └┘ └──┘ ┴ └┘ └┘ └──┘ └─
par └───────────┘ └┘ └──┘ ┴ └┘ └┘ └──┘ └─
pid └┘ └┘ └──┘ ┴ └┘ └┘ └──┘ └─
st ──────────────────────────────────────────────────────────────────────────────────────────────
522 (inv_le_inv norm_x_pos norm_r_pos).2, le_refl],
id └────────┘ └────────┘ └────────┘ └─────┘
src ────────────────┘ └────────┘┴ ┴ └───┘└─────┘┴
typ ────────────────┘ └────────┘┴└────────┘┴└────────┘└───┘└─────┘┴
doc ────────────────┘ ┴ ┴ └───┘ ┴
txt ────────────────┘ ┴ ┴ └───┘ ┴
par ────────────────┘ ┴ ┴ └───┘ ┴
pid ────────────────┘ ┴ ┴ └───┘ ┴
st ──────────────────────────────────────────────────────────────┘└─
523 show ∥r - x∥ ≤ ε / 2 / 2 * ∥r∥ ^ 2,
id ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └┘
typ └───┘ ┴ ┴┴ ┴ ┴┴┴ └─┘ └─┘ ┴ ┴ ┴ └┘
doc └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └┘
txt └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └┘
par └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ └┘
pid └───┘ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴┴
st ─────────────────────────────────────┘
524 by { rw ← dist_eq_norm, exact le_trans (le_of_lt (mem_ball'.1 hx)) (min_le_left _ _) },
id └──────────┘ └──────┘ └──────┘ └───────┘ └┘ └─────────┘
src └───┘└──────────┘ └────┘└──────┘┴ └──────┘┴ └───────┘└─┘ └─┘ └─────────┘└────┘
typ └───┘└──────────┘ └────┘└──────┘┴ └──────┘┴ └───────┘└─┘└┘└─┘ └─────────┘└────┘
doc └───┘ └────┘ ┴ ┴ └─┘ └─┘ └────┘
txt └───┘ └────┘ ┴ ┴ └─┘ └─┘ └────┘
par └───┘ └────┘ ┴ ┴ └─┘ └─┘ └────┘
pid └─┘ ┴ ┴ ┴ └─┘ └─┘ └───┘┴
st ┴└────────────────┘└─────────────────────────────────────────────────────────────┘└┘└
525 show ∥x∥⁻¹ ≤ 2 * ∥r∥⁻¹,
id ┴ ┴
src └───┘ ┴ └─┘ ┴
typ └───┘ ┴ ┴ └─┘ ┴ ┴
doc └───┘ ┴ └─┘ ┴
txt └───┘ ┴ └─┘ ┴
par └───┘ ┴ └─┘ ┴
pid └───┘ ┴ └─┘ ┴
st ─────────────────────────┘└─
526 { convert (inv_le_inv norm_x_pos (half_pos norm_r_pos)).2 rx,
id └────────┘ └────────┘ └──────┘ └────────┘ └┘
src └──────┘ └────────┘┴ ┴ └──────┘┴ └───┘
typ └──────┘ └────────┘┴└────────┘┴ └──────┘┴└────────┘└───┘└┘
doc └──────┘ ┴ ┴ ┴ └───┘
txt └──────┘ ┴ ┴ ┴ └───┘
par └──────┘ ┴ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ └───┘
st ─────┘└────────────────────────────────────────────────────────┘└─
527 rw [inv_div (ne.symm (ne_of_lt norm_r_pos)), div_eq_inv_mul, mul_comm],
id └─────┘ └─────┘ └──────┘ └────────┘ └────────────┘ └──────┘
src └──┘└─────┘┴ └─────┘┴ └──────┘┴ └──┘└────────────┘└┘└──────┘┴
typ └──┘└─────┘┴ └─────┘┴ └──────┘┴└────────┘└──┘└────────────┘└┘└──────┘┴
doc └──┘ ┴ ┴ ┴ └──┘ └┘ ┴
txt └──┘ ┴ ┴ ┴ └──┘ └┘ ┴
par └──┘ ┴ ┴ ┴ └──┘ └┘ ┴
pid └┘ ┴ ┴ ┴ └──┘ └┘ ┴
st ────────────────────────────────────────────────┘└──────────────┘└────────┘└──
528 norm_num },
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st ──────────────┘└┘└
529 show (0 : ℝ) ≤ 2, by norm_num
src └───┘ └──┘ └┘ └┘ └────────
typ └───┘ └──┘ └┘ └┘ └────────
doc └───┘ └──┘ └┘ └┘ └────────
txt └───┘ └──┘ └┘ └┘ └────────
par └───┘ └──┘ └┘ └┘ └────────
pid └───┘ └──┘ └┘ ┴┴ └
st ───────────────────┘
530 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st └─┘└
531 ... = ε/2 * (∥r∥ * ∥r∥⁻¹)^2 : by { generalize : ∥r∥⁻¹ = u, ring }
id ┴
src └───────────┘ ┴ ┴ └───┘
typ └───────────┘ ┴ ┴ ┴ └───┘
doc └───────────┘ ┴ ┴ └───┘
txt └───────────┘ ┴ ┴ └───┘
par └───────────┘ ┴ ┴ └───┘
pid ┴┴┴ ┴ ┴ ┴
st ─────────────────────────────────┘└───────────────────────┘└─────┘└┘
532 ... = ε/2 : by { rw [mul_inv_cancel (ne.symm (ne_of_lt norm_r_pos))], simp }
id └────────────┘ └─────┘ └──────┘ └────────┘
src └──┘└────────────┘┴ └─────┘┴ └──────┘┴ └─┘ └───┘
typ └──┘└────────────┘┴ └─────┘┴ └──────┘┴└────────┘└─┘ └───┘
doc └──┘ ┴ ┴ ┴ └─┘ └───┘
txt └──┘ ┴ ┴ ┴ └─┘ └───┘
par └──┘ ┴ ┴ ┴ └─┘ └───┘
pid └┘ ┴ ┴ ┴ └─┘ ┴
st └──────────────┘└───────────────────────────────────────────────────┘└──────┘└┘
533 ... < ε : half_lt_self εpos
id └──────────┘ └──┘
src └──────────┘
typ └──────────┘ └──┘
st └───────────────────────────┘└
534 end
st ──┘
535
536 lemma continuous_on_inv [normed_field α] : continuous_on (λ(x:α), x⁻¹) {x | x ≠ 0} :=
id └──────────┘ ┴ └───────────┘ ┴ ┴└┘ ┴┴ ┴ ┴
src └──────────┘ └───────────┘ └┘ ┴ ┴
typ └──────────┘ ┴ └───────────┘ ┴ ┴└┘ ┴┴ ┴ ┴
doc └──────────┘ └───────────┘
537 begin
st └─────
538 assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
539 apply continuous_at.continuous_within_at,
id └────────────────────────────────┘
src └────┘└────────────────────────────────┘
typ └────┘└────────────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────────────┘└─
540 exact (tendsto_inv hx)
id └─────────┘ └┘
src └────┘ └─────────┘┴ └┘
typ └────┘ └─────────┘┴└┘└┘
doc └────┘ ┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴ ┴ ┴┴
st ────────────────────────┘
541 end
st └─┘
542
543 instance : normed_field ℝ :=
id └──────────┘ ┴
src └──────────┘ ┴
typ └──────────┘ ┴
doc └──────────┘
544 { norm := λ x, abs x,
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
545 dist_eq := assume x y, rfl,
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
546 norm_mul' := abs_mul }
id └─────┘
src └─────┘
typ └─────┘
547
548 instance : nondiscrete_normed_field ℝ :=
id └──────────────────────┘ ┴
src └──────────────────────┘ ┴
typ └──────────────────────┘ ┴
doc └──────────────────────┘
549 { non_trivial := ⟨2, by { unfold norm, rw abs_of_nonneg; norm_num }⟩ }
id └───────────┘
src └─────────┘ └─┘└───────────┘ └───────┘
typ └─────────┘ └─┘└───────────┘ └───────┘
doc └─────────┘ └─┘ └───────┘
txt └─────────┘ └─┘ └───────┘
par └─────────┘ └─┘ └───────┘
pid └───┘ ┴ ┴
st └────────────┘└───────────────────────────┘└┘
550 end normed_field
551
552 /-- If a function converges to a nonzero value, its inverse converges to the inverse of this value.
553 We use the name `tendsto.inv'` as `tendsto.inv` is already used in multiplicative topological
554 groups. -/
555 lemma filter.tendsto.inv' [normed_field α] {l : filter β} {f : β → α} {y : α}
id └──────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └──────────┘ └────┘
typ └──────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc └──────────┘
556 (hy : y ≠ 0) (h : tendsto f l (𝓝 y)) :
id ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘ ┴
557 tendsto (λx, (f x)⁻¹) l (𝓝 y⁻¹) :=
id └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴└┘
src └─────┘ └┘ ┴ └┘
typ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴└┘
doc └─────┘ ┴
558 (normed_field.tendsto_inv hy).comp h
id └──────────────────────┘ └┘ └──┘ ┴
src └──────────────────────┘ └──┘
typ └──────────────────────┘ └┘ └──┘ ┴
559
560 lemma filter.tendsto.div [normed_field α] {l : filter β} {f g : β → α} {x y : α}
id └──────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └──────────┘ └────┘
typ └──────────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc └──────────┘
561 (hf : tendsto f l (𝓝 x)) (hg : tendsto g l (𝓝 y)) (hy : y ≠ 0) :
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─────┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └─────┘ ┴
562 tendsto (λa, f a / g a) l (𝓝 (x / y)) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴
563 hf.mul (hg.inv' hy)
id └┘└──┘ └┘└───┘ └┘
src └──┘ └───┘
typ └┘└──┘ └┘└───┘ └┘
doc └───┘
564
565 lemma real.norm_eq_abs (r : ℝ) : norm r = abs r := rfl
id ┴ └──┘ ┴ ┴ └─┘ ┴ └─┘
src ┴ └──┘ ┴ └─┘ └─┘
typ ┴ └──┘ ┴ ┴ └─┘ ┴ └─┘
566
567 @[simp] lemma norm_norm [normed_group α] (x : α) : ∥∥x∥∥ = ∥x∥ :=
id └──────────┘ ┴ ┴ └┘┴└┘ ┴ ┴┴┴
src └──────────┘ └┘ └┘ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴┴
doc └──┘ └──────────┘
568 by rw [real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)]
id └──────────────┘ └───────────┘ └─────────┘
src └──┘└──────────────┘└┘└───────────┘┴ └─────────┘└────
typ └──┘└──────────────┘└┘└───────────┘┴ └─────────┘└────
doc └──┘ └┘ ┴ └────
txt └──┘ └┘ ┴ └────
par └──┘ └┘ ┴ └────
pid └┘ └┘ ┴ └──┘└
st └───────────────────┘└─────────────────────────────┘┴└
569
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
570 @[simp] lemma nnnorm_norm [normed_group α] (a : α) : nnnorm ∥a∥ = nnnorm a :=
id └──────────┘ ┴ ┴ └────┘ ┴┴┴ ┴ └────┘ ┴
src └──────────┘ └────┘ ┴ ┴ ┴ └────┘
typ └──────────┘ ┴ ┴ └────┘ ┴┴┴ ┴ └────┘ ┴
doc └──┘ └──────────┘ └────┘ └────┘
571 by simp only [nnnorm, norm_norm]
id └────┘ └───────┘
src └─────────┘└────┘└┘└───────┘└─
typ └─────────┘└────┘└┘└───────┘└─
doc └─────────┘└────┘└┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └──────────────────────────────
572
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
573 instance : normed_ring ℤ :=
id └─────────┘ ┴
src └─────────┘ ┴
typ └─────────┘ ┴
doc └─────────┘
574 { norm := λ n, ∥(n : ℝ)∥,
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
575 norm_mul := λ m n, le_of_eq $ by simp only [norm, int.cast_mul, abs_mul],
id ┴ ┴ └──────┘ └──────────┘ └─────┘
src └──────┘ └─────────┘ └┘└──────────┘└┘└─────┘┴
typ ┴ ┴ └──────┘ └─────────┘ └┘└──────────┘└┘└─────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └──────────────────────────────────────┘
576 dist_eq := λ m n, by simp only [int.dist_eq, norm, int.cast_sub] }
id ┴ ┴ └─────────┘ └──────────┘
src └─────────┘└─────────┘└┘ └┘└──────────┘└┘
typ ┴ ┴ └─────────┘└─────────┘└┘ └┘└──────────┘└┘
doc └─────────┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st └───────────────────────────────────────────┘
577
578 @[elim_cast] lemma int.norm_cast_real (m : ℤ) : ∥(m : ℝ)∥ = ∥m∥ := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─┘
doc └───────┘
579
580 instance : normed_field ℚ :=
id └──────────┘ ┴
src └──────────┘ ┴
typ └──────────┘ ┴
doc └──────────┘ ┴
581 { norm := λ r, ∥(r : ℝ)∥,
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
582 norm_mul' := λ r₁ r₂, by simp only [norm, rat.cast_mul, abs_mul],
id └┘ └┘ └──────────┘ └─────┘
src └─────────┘ └┘└──────────┘└┘└─────┘┴
typ └┘ └┘ └─────────┘ └┘└──────────┘└┘└─────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └──────────────────────────────────────┘
583 dist_eq := λ r₁ r₂, by simp only [rat.dist_eq, norm, rat.cast_sub] }
id └┘ └┘ └─────────┘ └──────────┘
src └─────────┘└─────────┘└┘ └┘└──────────┘└┘
typ └┘ └┘ └─────────┘└─────────┘└┘ └┘└──────────┘└┘
doc └─────────┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st └───────────────────────────────────────────┘
584
585 instance : nondiscrete_normed_field ℚ :=
id └──────────────────────┘ ┴
src └──────────────────────┘ ┴
typ └──────────────────────┘ ┴
doc └──────────────────────┘ ┴
586 { non_trivial := ⟨2, by { unfold norm, rw abs_of_nonneg; norm_num }⟩ }
id └───────────┘
src └─────────┘ └─┘└───────────┘ └───────┘
typ └─────────┘ └─┘└───────────┘ └───────┘
doc └─────────┘ └─┘ └───────┘
txt └─────────┘ └─┘ └───────┘
par └─────────┘ └─┘ └───────┘
pid └───┘ ┴ ┴
st └────────────┘└───────────────────────────┘└┘
587
588 @[elim_cast, simp] lemma rat.norm_cast_real (r : ℚ) : ∥(r : ℝ)∥ = ∥r∥ := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─┘
doc └───────┘ └──┘ ┴
589
590 @[elim_cast, simp] lemma int.norm_cast_rat (m : ℤ) : ∥(m : ℚ)∥ = ∥m∥ :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴
doc └───────┘ └──┘ ┴
591 by rw [← rat.norm_cast_real, ← int.norm_cast_real]; congr' 1; norm_cast
id └────────────────┘ └────────────────┘
src └────┘└────────────────┘└──┘└────────────────┘┴ └──────┘ └─────────
typ └────┘└────────────────┘└──┘└────────────────┘┴ └──────┘ └─────────
doc └────┘ └──┘ ┴ └──────┘ └─────────
txt └────┘ └──┘ ┴ └──────┘ └─────────
par └────┘ └──┘ ┴ └──────┘ └─────────
pid └──┘ └──┘ ┴ ┴┴ └
st └───────────────────────┘└────────────────────┘┴└─────────────────────
592
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
593 section normed_space
594
595 section prio
596 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
597 -- see Note[vector space definition] for why we extend `module`.
598 /-- A normed space over a normed field is a vector space endowed with a norm which satisfies the
599 equality `∥c • x∥ = ∥c∥ ∥x∥`. -/
600 class normed_space (α : Type*) (β : Type*) [normed_field α] [normed_group β]
id └───┘ └───┘ └──────────┘ ┴ └──────────┘ ┴
src └──────────┘ └──────────┘
typ └───┘ └───┘ └──────────┘ ┴ └──────────┘ ┴
doc └──────────┘ └──────────┘
601 extends module α β :=
id └────┘ ┴ ┴
src └────┘
typ └────┘ ┴ ┴
doc └────┘
602 (norm_smul : ∀ (a:α) (b:β), norm (a • b) = has_norm.norm a * norm b)
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ ┴ └───────────┘ ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └──┘ ┴
603 end prio
604
605 variables [normed_field α] [normed_group β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
606
607 instance normed_field.to_normed_space : normed_space α α :=
id └──────────┘ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴
doc └──────────┘
608 { norm_smul := normed_field.norm_mul }
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
609
610 set_option class.instance_max_depth 43
doc └──────────────────────┘
611
612 lemma norm_smul [normed_space α β] (s : α) (x : β) : ∥s • x∥ = ∥s∥ * ∥x∥ :=
id └──────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
doc └──────────┘
613 normed_space.norm_smul s x
id └────────────────────┘ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴
614
615 lemma dist_smul [normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) = ∥s∥ * dist x y :=
id └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └──┘ ┴ ┴
src └──────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ └──────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ └──┘ ┴ ┴
doc └──────────┘
616 by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
id └──────────┘ └───────┘ └──────┘
src └─────────┘└──────────┘└┘ └───────┘└──────────┘└──────┘└─
typ └─────────┘└──────────┘└┘ └───────┘└──────────┘└──────┘└─
doc └─────────┘ └┘ └──────────┘ └─
txt └─────────┘ └┘ └──────────┘ └─
par └─────────┘ └┘ └──────────┘ └─
pid ┴└──┘└┘ └┘ └──────────┘ ┴└
st └─────────────────────────────────────────────────────────
617
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
618 lemma nnnorm_smul [normed_space α β] (s : α) (x : β) : nnnorm (s • x) = nnnorm s * nnnorm x :=
id └──────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
src └──────────┘ └────┘ ┴ ┴ └────┘ ┴ └────┘
typ └──────────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴
doc └──────────┘ └────┘ └────┘ └────┘
619 nnreal.eq $ norm_smul s x
id └───────┘ └───────┘ ┴ ┴
src └───────┘ └───────┘
typ └───────┘ └───────┘ ┴ ┴
620
621 variables {E : Type*} {F : Type*}
id ┴
typ ┴
622 [normed_group E] [normed_space α E] [normed_group F] [normed_space α F]
id └──────────┘ └──────────┘ └──────────┘ └──────────┘
src └──────────┘ └──────────┘ └──────────┘ └──────────┘
typ └──────────┘ └──────────┘ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘ └──────────┘ └──────────┘
623
624 lemma tendsto_smul {f : γ → α} { g : γ → F} {e : filter γ} {s : α} {b : F} :
id ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
625 (tendsto f e (𝓝 s)) → (tendsto g e (𝓝 b)) → tendsto (λ x, (f x) • (g x)) e (𝓝 (s • b)) :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └─────┘ ┴ └─────┘ ┴
626 begin
st └─────
627 intros limf limg,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────┘└─
628 rw tendsto_iff_norm_tendsto_zero,
id └───────────────────────────┘
src └─┘└───────────────────────────┘
typ └─┘└───────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────────────┘└─
629 have ineq := λ x : γ, calc
id ┴
src └───────────┘ └───┘ └┘ └
typ └───────────┘ └───┘┴└┘ └
doc └───────────┘ └───┘ └┘ └
txt └───────────┘ └───┘ └┘ └
par └───────────┘ └───┘ └┘ └
pid └───────┘┴└─┘ └───┘ └┘ └
st ─────────────────────────────
630 ∥f x • g x - s • b∥ = ∥(f x • g x - s • g x) + (s • g x - s • b)∥ : by simp[add_assoc]
id ┴ ┴ ┴ ┴ └───────┘
src ─────┘┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└───┘└───────┘└─
typ ─────┘┴ ┴ ┴┴┴ ┴ ┴┴┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└───┘└───────┘└─
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└───┘ └─
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└───┘ └─
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└───┘ └─
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └────┘ └─
st ───────────────────────────────────────────────────────────────────────────┘└────────────────
631 ... ≤ ∥f x • g x - s • g x∥ + ∥s • g x - s • b∥ : norm_add_le (f x • g x - s • g x) (s • g x - s • b)
id ┴ └─────────┘ ┴ ┴ ┴ ┴
src ─────────────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└─────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
typ ─────────────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└─────────┘┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴┴ ┴ ┴┴┴ ┴┴└─
doc ─────────────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└─────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt ─────────────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ─────────────────────┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ─────────────────────┘└─────────────────────────────────────────────────────────────────────────────────────────────────────
632 ... ≤ ∥f x - s∥*∥g x∥ + ∥s∥*∥g x - b∥ : by { rw [←smul_sub, ←sub_smul, norm_smul, norm_smul] },
id ┴ └──────┘ └──────┘ └───────┘ └───────┘
src ─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘└───┘└──────┘└─┘└──────┘└┘└───────┘└┘└───────┘└┘┴
typ ─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘└───┘└──────┘└─┘└──────┘└┘└───────┘└┘└───────┘└┘┴
doc ─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘└───┘ └─┘ └┘ └┘ └┘┴
txt ─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘└───┘ └─┘ └┘ └┘ └┘┴
par ─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘└───┘ └─┘ └┘ └┘ └┘┴
pid ─────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────┘ └─┘ └┘ └┘ └─┘
st ───────────────────────────────────────────────────────────────┘└──────────────┘└─────────┘└─────────┘└─────────┘┴┴└┘└
633 apply squeeze_zero,
id └──────────┘
src └────┘└──────────┘
typ └────┘└──────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────┘└─
634 { intro t, exact norm_nonneg _ },
id └─────────┘
src └─────┘ └────┘└─────────┘└─┘
typ └─────┘ └────┘└─────────┘└─┘
doc └─────┘ └────┘ └─┘
txt └─────┘ └────┘ └─┘
par └─────┘ └────┘ └─┘
pid └┘ ┴ └┘┴
st ───┘└─────┘└────────────────────┘└┘└
635 { exact ineq },
id └──┘
src └────┘ ┴
typ └────┘└──┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└─────────┘└┘└
636 { clear ineq,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └───┘
st ─────────────┘└─
637
st ─
638 have limf': tendsto (λ x, ∥f x - s∥) e (𝓝 0) := tendsto_iff_norm_tendsto_zero.1 limf,
id └─────┘ ┴ ┴ ┴ ┴ └───────────────────────────┘ └──┘
src └──────────┘└─────┘┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴└─────┘└───────────────────────────┘└─┘
typ └──────────┘└─────┘┴ └──┘ ┴┴ ┴ ┴┴ └┘┴┴ ┴└─────┘└───────────────────────────┘└─┘└──┘
doc └──────────┘└─────┘┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴└─────┘ └─┘
txt └──────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └─────┘ └─┘
par └──────────┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └─────┘ └─┘
pid └────────┘└┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ └─┘└──┘ └─┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
639 have limg' : tendsto (λ x, ∥g x∥) e (𝓝 ∥b∥) := filter.tendsto.comp (continuous_iff_continuous_at.1 continuous_norm _) limg,
id └─────┘ ┴ ┴ ┴ └─────────────────┘ └──────────────────────────┘ └─────────────┘ └──┘
src └───────────┘└─────┘┴ └──┘ ┴ └┘ ┴ ┴ └───┘└─────────────────┘┴ └──────────────────────────┘└─┘└─────────────┘└──┘
typ └───────────┘└─────┘┴ └──┘ ┴┴ └┘┴┴ ┴ ┴ └───┘└─────────────────┘┴ └──────────────────────────┘└─┘└─────────────┘└──┘└──┘
doc └───────────┘└─────┘┴ └──┘ ┴ └┘ ┴ ┴ └───┘ ┴ └─┘ └──┘
txt └───────────┘ ┴ └──┘ ┴ └┘ ┴ ┴ └───┘ ┴ └─┘ └──┘
par └───────────┘ ┴ └──┘ ┴ └┘ ┴ ┴ └───┘ ┴ └─┘ └──┘
pid └────────┘└─┘ ┴ └──┘ ┴ └┘ ┴ ┴ ┴└──┘ ┴ └─┘ └──┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
640
st ─
641 have lim1 := limf'.mul limg',
id └───────┘ └───┘
src └───────────┘└───────┘┴
typ └───────────┘└───────┘┴└───┘
doc └───────────┘ ┴
txt └───────────┘ ┴
par └───────────┘ ┴
pid └───────┘┴└─┘ ┴
st ───────────────────────────────┘└─
642 simp only [zero_mul, sub_eq_add_neg] at lim1,
id └──────┘ └────────────┘
src └─────────┘└──────┘└┘└────────────┘└───────┘
typ └─────────┘└──────┘└┘└────────────┘└───────┘
doc └─────────┘ └┘ └───────┘
txt └─────────┘ └┘ └───────┘
par └─────────┘ └┘ └───────┘
pid ┴└──┘└┘ └┘ ┴┴└─────┘
st ───────────────────────────────────────────────┘└─
643
st ─
644 have limg3 := tendsto_iff_norm_tendsto_zero.1 limg,
id └───────────────────────────┘ └──┘
src └────────────┘└───────────────────────────┘└─┘
typ └────────────┘└───────────────────────────┘└─┘└──┘
doc └────────────┘ └─┘
txt └────────────┘ └─┘
par └────────────┘ └─┘
pid └────────┘┴└─┘ └─┘
st ─────────────────────────────────────────────────────┘└─
645
st ─
646 have lim2 := (tendsto_const_nhds : tendsto _ _ (𝓝 ∥ s ∥)).mul limg3,
id └────────────────┘ └─────┘ ┴ └───┘
src └───────────┘ └────────────────┘└─┘└─────┘└───┘ ┴ ┴ ┴ └─────┘
typ └───────────┘ └────────────────┘└─┘└─────┘└───┘ ┴ ┴┴┴ └─────┘└───┘
doc └───────────┘ └─┘└─────┘└───┘ ┴ ┴ ┴ └─────┘
txt └───────────┘ └─┘ └───┘ ┴ ┴ ┴ └─────┘
par └───────────┘ └─┘ └───┘ ┴ ┴ ┴ └─────┘
pid └───────┘┴└─┘ └─┘ └───┘ ┴ ┴ ┴ └─────┘
st ──────────────────────────────────────────────────────────────────────┘└─
647 simp only [sub_eq_add_neg, mul_zero] at lim2,
id └────────────┘ └──────┘
src └─────────┘└────────────┘└┘└──────┘└───────┘
typ └─────────┘└────────────┘└┘└──────┘└───────┘
doc └─────────┘ └┘ └───────┘
txt └─────────┘ └┘ └───────┘
par └─────────┘ └┘ └───────┘
pid ┴└──┘└┘ └┘ ┴┴└─────┘
st ───────────────────────────────────────────────┘└─
648
st ─
649 rw [show (0:ℝ) = 0 + 0, by simp],
id ┴
src └──┘ ┴ └┘ └┘┴└─┘ └─────┘└──┘┴
typ └──┘ ┴ └┘ └┘┴└─┘ └─────┘└──┘┴
doc └──┘ ┴ └┘ └┘ └─┘ └─────┘└──┘┴
txt └──┘ ┴ └┘ └┘ └─┘ └─────┘└──┘┴
par └──┘ ┴ └┘ └┘ └─┘ └─────┘└──┘┴
pid └┘ ┴ └┘ └┘ └─┘ └──────────┘
st ─────────────────────────────┘└───┘└──
650 exact lim1.add lim2 }
id └──────┘ └──┘
src └────┘└──────┘┴ └┘
typ └────┘└──────┘┴└──┘└┘
doc └────┘ ┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴ ┴ └┘
st ────────────────────────┘└─
651 end
st ──┘
652
653 lemma tendsto_smul_const {g : γ → F} {e : filter γ} (s : α) {b : F} :
id ┴ ┴ └────┘ ┴ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴ ┴
654 (tendsto g e (𝓝 b)) → tendsto (λ x, s • (g x)) e (𝓝 (s • b)) :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └─────┘ ┴
655 tendsto_smul tendsto_const_nhds
id └──────────┘ └────────────────┘
src └──────────┘ └────────────────┘
typ └──────────┘ └────────────────┘
656
657 @[priority 100] -- see Note [lower instance priority]
658 instance normed_space.topological_vector_space : topological_vector_space α E :=
id └──────────────────────┘ ┴ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴ ┴
doc └──────────────────────┘
659 { continuous_smul := continuous_iff_continuous_at.2 $ λp, tendsto_smul
id └──────────────────────────┘┴ ┴ └──────────┘
src └──────────────────────────┘┴ └──────────┘
typ └──────────────────────────┘┴ ┴ └──────────┘
660 (continuous_iff_continuous_at.1 continuous_fst _) (continuous_iff_continuous_at.1 continuous_snd _) }
id └──────────────────────────┘┴ └────────────┘ └──────────────────────────┘┴ └────────────┘
src └──────────────────────────┘┴ └────────────┘ └──────────────────────────┘┴ └────────────┘
typ └──────────────────────────┘┴ └────────────┘ └──────────────────────────┘┴ └────────────┘
661
662 open normed_field
663
664 /-- If there is a scalar `c` with `∥c∥>1`, then any element can be moved by scalar multiplication to
665 any shell of width `∥c∥`. Also recap information on the norm of the rescaling element that shows
666 up in applications. -/
667 lemma rescale_to_shell {c : α} (hc : 1 < ∥c∥) {ε : ℝ} (εpos : 0 < ε) {x : E} (hx : x ≠ 0) :
id ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴
668 ∃d:α, d ≠ 0 ∧ ∥d • x∥ ≤ ε ∧ (ε/∥c∥ ≤ ∥d • x∥) ∧ (∥d∥⁻¹ ≤ ε⁻¹ * ∥c∥ * ∥x∥) :=
id ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴└┘ ┴ ┴└┘ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴┴┴┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴└┘ ┴ ┴└┘ ┴ ┴┴┴ ┴ ┴┴┴
669 begin
st └─────
670 have xεpos : 0 < ∥x∥/ε := div_pos_of_pos_of_pos ((norm_pos_iff _).2 hx) εpos,
id ┴ ┴┴┴┴┴ └───────────────────┘ └──────────┘ └┘ └──┘
src └─────────────┘┴┴┴ ┴┴ └──┘└───────────────────┘┴ └──────────┘└────┘ └┘
typ └─────────────┘┴┴┴┴┴┴┴└──┘└───────────────────┘┴ └──────────┘└────┘└┘└┘└──┘
doc └─────────────┘ ┴ └──┘ ┴ └────┘ └┘
txt └─────────────┘ ┴ └──┘ ┴ └────┘ └┘
par └─────────────┘ ┴ └──┘ ┴ └────┘ └┘
pid └────────┘└───┘ ┴ └──┘ ┴ └────┘ └┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
671 rcases exists_int_pow_near xεpos hc with ⟨n, hn⟩,
id └─────────────────┘ └───┘ └┘
src └─────┘└─────────────────┘┴ ┴ └───────────┘
typ └─────┘└─────────────────┘┴└───┘┴└┘└───────────┘
doc └─────┘└─────────────────┘┴ ┴ └───────────┘
txt └─────┘ ┴ ┴ └───────────┘
par └─────┘ ┴ ┴ └───────────┘
pid ┴ ┴ ┴ └───────────┘
st ─────────────────────────────────────────────────┘└─
672 have cpos : 0 < ∥c∥ := lt_trans (zero_lt_one : (0 :ℝ) < 1) hc,
id ┴ └──────┘ └─────────┘ └┘
src └────────────┘ ┴ └──┘└──────┘┴ └─────────┘└─┘ └─┘ └┘ └──┘
typ └────────────┘ ┴ ┴ └──┘└──────┘┴ └─────────┘└─┘ └─┘ └┘ └──┘└┘
doc └────────────┘ ┴ └──┘ ┴ └─┘ └─┘ └┘ └──┘
txt └────────────┘ ┴ └──┘ ┴ └─┘ └─┘ └┘ └──┘
par └────────────┘ ┴ └──┘ ┴ └─┘ └─┘ └┘ └──┘
pid └───────┘└───┘ ┴ └──┘ ┴ └─┘ └─┘ └┘ └──┘
st ──────────────────────────────────────────────────────────────┘└─
673 have cnpos : 0 < ∥c^(n+1)∥ := by { rw norm_fpow, exact lt_trans xεpos hn.2 },
id ┴┴ ┴┴ └───────┘ └──────┘ └───┘ └┘
src └─────────────┘ ┴ ┴ ┴└┘ └──┘ └─┘└─┘└───────┘└┘└────┘└──────┘┴ ┴ └─┘┴
typ └─────────────┘ ┴ ┴┴ ┴┴└┘ └──┘ └─┘└─┘└───────┘└┘└────┘└──────┘┴└───┘┴└┘└─┘┴
doc └─────────────┘ ┴ └┘ └──┘ └─┘└─┘ └┘└────┘ ┴ ┴ └─┘┴
txt └─────────────┘ ┴ └┘ └──┘ └─┘└─┘ └┘└────┘ ┴ ┴ └─┘┴
par └─────────────┘ ┴ └┘ └──┘ └─┘└─┘ └┘└────┘ ┴ ┴ └─┘┴
pid └────────┘└───┘ ┴ └┘ └──┘ └────┘ └──────┘ ┴ ┴ └──┘
st ─────────────────────────────────┘└─────────────┘└──────────────────────────┘└┘└
674 refine ⟨(c^(n+1))⁻¹, _, _, _, _⟩,
id ┴ ┴ └┘
src └─────┘ └─┘└┘└───────────┘
typ └─────┘ ┴ ┴ └─┘└┘└───────────┘
doc └─────┘ └─┘ └───────────┘
txt └─────┘ └─┘ └───────────┘
par └─────┘ └─┘ └───────────┘
pid ┴ └─┘ └───────────┘
st ─────────────────────────────────┘└─
675 show (c ^ (n + 1))⁻¹ ≠ 0,
id ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ └──┘ └┘┴└┘
typ └───┘ ┴┴ ┴ ┴┴ └──┘ └┘┴└┘
doc └───┘ ┴ ┴ ┴ └──┘ └┘ └┘
txt └───┘ ┴ ┴ ┴ └──┘ └┘ └┘
par └───┘ ┴ ┴ ┴ └──┘ └┘ └┘
pid └───┘ ┴ ┴ ┴ └──┘ └┘ ┴┴
st ──────────────────────────┘
676 by rwa [ne.def, inv_eq_zero, ← ne.def, ← norm_pos_iff],
id └────┘ └─────────┘ └────┘ └──────────┘
src └───┘└────┘└┘└─────────┘└──┘└────┘└──┘└──────────┘┴
typ └───┘└────┘└┘└─────────┘└──┘└────┘└──┘└──────────┘┴
doc └───┘ └┘ └──┘ └──┘ ┴
txt └───┘ └┘ └──┘ └──┘ ┴
par └───┘ └┘ └──┘ └──┘ ┴
pid └┘ └┘ └──┘ └──┘ ┴
st └────┘└───────────┘└────────┘└──────────────┘┴└─
677 show ∥(c ^ (n + 1))⁻¹ • x∥ ≤ ε,
id ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ └──┘ ┴┴┴ ┴┴┴
typ └───┘ ┴┴ ┴ ┴┴ └──┘ ┴┴┴┴ ┴┴┴┴
doc └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────
678 { rw [norm_smul, norm_inv, ← div_eq_inv_mul, div_le_iff cnpos, mul_comm, norm_fpow],
id └───────┘ └──────┘ └────────────┘ └────────┘ └───┘ └──────┘ └───────┘
src └──┘└───────┘└┘└──────┘└──┘└────────────┘└┘└────────┘┴ └┘└──────┘└┘└───────┘┴
typ └──┘└───────┘└┘└──────┘└──┘└────────────┘└┘└────────┘┴└───┘└┘└──────┘└┘└───────┘┴
doc └──┘ └┘ └──┘ └┘ ┴ └┘ └┘ ┴
txt └──┘ └┘ └──┘ └┘ ┴ └┘ └┘ ┴
par └──┘ └┘ └──┘ └┘ ┴ └┘ └┘ ┴
pid └┘ └┘ └──┘ └┘ ┴ └┘ └┘ ┴
st ───┘└───────────┘└────────┘└────────────────┘└────────────────┘└────────┘└─────────┘└──
679 exact (div_le_iff εpos).1 (le_of_lt (hn.2)) },
id └────────┘ └──┘ └──────┘ └┘
src └────┘ └────────┘┴ └──┘ └──────┘┴ └───┘
typ └────┘ └────────┘┴└──┘└──┘ └──────┘┴ └┘└───┘
doc └────┘ ┴ └──┘ ┴ └───┘
txt └────┘ ┴ └──┘ ┴ └───┘
par └────┘ ┴ └──┘ ┴ └───┘
pid ┴ ┴ └──┘ ┴ └──┘┴
st ───────────────────────────────────────────────┘└┘└
680 show ε / ∥c∥ ≤ ∥(c ^ (n + 1))⁻¹ • x∥,
id ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
typ └───┘┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ └──┘ ┴ ┴┴
doc └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
st ────────────────────────────────────────
681 { rw [div_le_iff cpos, norm_smul, norm_inv, norm_fpow, fpow_add (ne_of_gt cpos),
id └────────┘ └──┘ └───────┘ └──────┘ └───────┘ └──────┘ └──────┘ └──┘
src └──┘└────────┘┴ └┘└───────┘└┘└──────┘└┘└───────┘└┘└──────┘┴ └──────┘┴ └──
typ └──┘└────────┘┴└──┘└┘└───────┘└┘└──────┘└┘└───────┘└┘└──────┘┴ └──────┘┴└──┘└──
doc └──┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └──
txt └──┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └──
par └──┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └──
pid └┘ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └──
st ───┘└─────────────────┘└─────────┘└────────┘└─────────┘└────────────────────────┘└─
682 fpow_one, mul_inv', mul_comm, ← mul_assoc, ← mul_assoc, mul_inv_cancel (ne_of_gt cpos),
id └──────┘ └──────┘ └──────┘ └───────┘ └───────┘ └────────────┘ └──────┘ └──┘
src ───────┘└──────┘└┘└──────┘└┘└──────┘└──┘└───────┘└──┘└───────┘└┘└────────────┘┴ └──────┘┴ └──
typ ───────┘└──────┘└┘└──────┘└┘└──────┘└──┘└───────┘└──┘└───────┘└┘└────────────┘┴ └──────┘┴└──┘└──
doc ───────┘ └┘ └┘ └──┘ └──┘ └┘ ┴ ┴ └──
txt ───────┘ └┘ └┘ └──┘ └──┘ └┘ ┴ ┴ └──
par ───────┘ └┘ └┘ └──┘ └──┘ └┘ ┴ ┴ └──
pid ───────┘ └┘ └┘ └──┘ └──┘ └┘ ┴ ┴ └──
st ───────────────┘└────────┘└────────┘└───────────┘└───────────┘└──────────────────────────────┘└─
683 one_mul, ← div_eq_inv_mul, le_div_iff (fpow_pos_of_pos cpos _), mul_comm],
id └─────┘ └────────────┘ └────────┘ └─────────────┘ └──┘ └──────┘
src ───────┘└─────┘└──┘└────────────┘└┘└────────┘┴ └─────────────┘┴ └───┘└──────┘┴
typ ───────┘└─────┘└──┘└────────────┘└┘└────────┘┴ └─────────────┘┴└──┘└───┘└──────┘┴
doc ───────┘ └──┘ └┘ ┴ ┴ └───┘ ┴
txt ───────┘ └──┘ └┘ ┴ ┴ └───┘ ┴
par ───────┘ └──┘ └┘ ┴ ┴ └───┘ ┴
pid ───────┘ └──┘ └┘ ┴ ┴ └───┘ ┴
st ──────────────┘└────────────────┘└───────────────────────────────────┘└────────┘└──
684 exact (le_div_iff εpos).1 hn.1 },
id └────────┘ └──┘ └┘
src └────┘ └────────┘┴ └──┘ └─┘
typ └────┘ └────────┘┴└──┘└──┘└┘└─┘
doc └────┘ ┴ └──┘ └─┘
txt └────┘ ┴ └──┘ └─┘
par └────┘ ┴ └──┘ └─┘
pid ┴ ┴ └──┘ └─┘
st ──────────────────────────────────┘└┘└
685 show ∥(c ^ (n + 1))⁻¹∥⁻¹ ≤ ε⁻¹ * ∥c∥ * ∥x∥,
id ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴┴┴ ┴ ┴
typ └───┘ ┴ ┴ ┴┴ └──┘ ┴ ┴┴ ┴┴┴ ┴ ┴ ┴ ┴
doc └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────
686 { have : ε⁻¹ * ∥c∥ * ∥x∥ = ε⁻¹ * ∥x∥ * ∥c∥, by ring,
id ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ └──┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────┘ └─
687 rw [norm_inv, inv_inv', norm_fpow, fpow_add (ne_of_gt cpos), fpow_one, this, ← div_eq_inv_mul],
id └──────┘ └──────┘ └───────┘ └──────┘ └──────┘ └──┘ └──────┘ └──┘ └────────────┘
src └──┘└──────┘└┘└──────┘└┘└───────┘└┘└──────┘┴ └──────┘┴ └─┘└──────┘└┘ └──┘└────────────┘┴
typ └──┘└──────┘└┘└──────┘└┘└───────┘└┘└──────┘┴ └──────┘┴└──┘└─┘└──────┘└┘└──┘└──┘└────────────┘┴
doc └──┘ └┘ └┘ └┘ ┴ ┴ └─┘ └┘ └──┘ ┴
txt └──┘ └┘ └┘ └┘ ┴ ┴ └─┘ └┘ └──┘ ┴
par └──┘ └┘ └┘ └┘ ┴ ┴ └─┘ └┘ └──┘ ┴
pid └┘ └┘ └┘ └┘ ┴ ┴ └─┘ └┘ └──┘ ┴
st ───────────────┘└────────┘└─────────┘└────────────────────────┘└────────┘└────┘└────────────────┘└──
688 exact mul_le_mul_of_nonneg_right hn.1 (norm_nonneg _) }
id └────────────────────────┘ └┘ └─────────┘
src └────┘└────────────────────────┘┴ └─┘ └─────────┘└──┘
typ └────┘└────────────────────────┘┴└┘└─┘ └─────────┘└──┘
doc └────┘ ┴ └─┘ └──┘
txt └────┘ ┴ └─┘ └──┘
par └────┘ ┴ └─┘ └──┘
pid ┴ ┴ └─┘ └─┘┴
st ─────────────────────────────────────────────────────────┘└─
689 end
st ──┘
690
691 /-- The product of two normed spaces is a normed space, with the sup norm. -/
692 instance : normed_space α (E × F) :=
id └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴ ┴
doc └──────────┘
693 { norm_smul :=
694 begin
st └─────
695 intros s x,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └──┘
st ─────────────┘└─
696 cases x with x₁ x₂,
id ┴
src └────┘ └─────────┘
typ └────┘┴└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ─────────────────────┘└─
697 change max (∥s • x₁∥) (∥s • x₂∥) = ∥s∥ * max (∥x₁∥) (∥x₂∥),
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └┘ └┘
src └─────┘ ┴ ┴ ┴┴┴ ┴└┘ ┴ ┴ └┘┴┴ ┴┴┴└─┘┴ └┘ ┴
typ └─────┘ ┴ ┴ ┴┴┴ ┴└┘ ┴ ┴ └┘┴┴ ┴ ┴┴┴└─┘┴ └┘ └┘ └┘ ┴
doc └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────┘└─
698 rw [norm_smul, norm_smul, ← mul_max_of_nonneg _ _ (norm_nonneg _)]
id └───────┘ └───────┘ └───────────────┘ └─────────┘
src └──┘└───────┘└┘└───────┘└──┘└───────────────┘└───┘ └─────────┘└────
typ └──┘└───────┘└┘└───────┘└──┘└───────────────┘└───┘ └─────────┘└────
doc └──┘ └┘ └──┘ └───┘ └────
txt └──┘ └┘ └──┘ └───┘ └────
par └──┘ └┘ └──┘ └───┘ └────
pid └┘ └┘ └──┘ └───┘ └──┘└
st ────────────────┘└─────────┘└───────────────────────────────────────┘┴└
699 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
700
701 add_smul := λ r x y, prod.ext (add_smul _ _ _) (add_smul _ _ _),
id ┴ ┴ ┴ └──────┘ └──────┘ └──────┘
src └──────┘ └──────┘ └──────┘
typ ┴ ┴ ┴ └──────┘ └──────┘ └──────┘
702 smul_add := λ r x y, prod.ext (smul_add _ _ _) (smul_add _ _ _),
id ┴ ┴ ┴ └──────┘ └──────┘ └──────┘
src └──────┘ └──────┘ └──────┘
typ ┴ ┴ ┴ └──────┘ └──────┘ └──────┘
703 ..prod.normed_group,
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
704 ..prod.module }
id └─────────┘
src └─────────┘
typ └─────────┘
705
706 /-- The product of finitely many normed spaces is a normed space, with the sup norm. -/
707 instance pi.normed_space {E : ι → Type*} [fintype ι] [∀i, normed_group (E i)]
id ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴
src └─────┘ └──────────┘
typ ┴ └─────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └─────┘ └──────────┘
708 [∀i, normed_space α (E i)] : normed_space α (Πi, E i) :=
id ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └──────────┘
typ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └──────────┘ └──────────┘
709 { norm_smul := λ a f,
id ┴ ┴
typ ┴ ┴
710 show (↑(finset.sup finset.univ (λ (b : ι), nnnorm (a • f b))) : ℝ) =
id ┴ └────────┘ └─────────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └────────┘ └─────────┘ └────┘ ┴ ┴ ┴
typ ┴ └────────┘ └─────────┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └─────────┘ └────┘
711 nnnorm a * ↑(finset.sup finset.univ (λ (b : ι), nnnorm (f b))),
id └────┘ ┴ ┴ ┴ └────────┘ └─────────┘ ┴ └────┘ ┴ ┴
src └────┘ ┴ ┴ └────────┘ └─────────┘ └────┘
typ └────┘ ┴ ┴ ┴ └────────┘ └─────────┘ ┴ └────┘ ┴ ┴
doc └────┘ └────────┘ └─────────┘ └────┘
712 by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul] }
id └────────────┘ └───────────────────┘ └─────────┘
src └─────────┘ └────────────┘└──────────┘└───────────────────┘└┘└─────────┘└┘
typ └─────────┘ └────────────┘└──────────┘└───────────────────┘└┘└─────────┘└┘
doc └─────────┘ └──────────┘ └┘ └┘
txt └─────────┘ └──────────┘ └┘ └┘
par └─────────┘ └──────────┘ └┘ └┘
pid ┴└──┘└┘ └──────────┘ └┘ ┴┴
st └─────────────────────────────────────────────────────────────────────────┘
713
714 /-- A subspace of a normed space is also a normed space, with the restriction of the norm. -/
715 instance submodule.normed_space {𝕜 : Type*} [normed_field 𝕜]
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
716 {E : Type*} [normed_group E] [normed_space 𝕜 E] (s : submodule 𝕜 E) : normed_space 𝕜 s :=
id └──────────┘ ┴ └──────────┘ ┴ ┴ └───────┘ ┴ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘ └───────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴ └───────┘ ┴ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘ └───────┘ └──────────┘
717 { norm_smul := λc x, norm_smul c (x : E) }
id ┴ ┴ └───────┘ ┴ ┴ ┴
src └───────┘
typ ┴ ┴ └───────┘ ┴ ┴ ┴
718
719 end normed_space
720
721 section normed_algebra
722
723 /-- A normed algebra `𝕜'` over `𝕜` is an algebra endowed with a norm for which the embedding of
724 `𝕜` in `𝕜'` is an isometry. -/
725 class normed_algebra (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_ring 𝕜']
id └───┘ └───┘ └──────────┘ ┴ └─────────┘ └┘
src └──────────┘ └─────────┘
typ └───┘ └───┘ └──────────┘ ┴ └─────────┘ └┘
doc └──────────┘ └─────────┘
726 extends algebra 𝕜 𝕜' :=
id └─────┘ ┴ └┘
src └─────┘
typ └─────┘ ┴ └┘
doc └─────┘
727 (norm_algebra_map_eq : ∀x:𝕜, ∥algebra_map 𝕜' x∥ = ∥x∥)
id ┴ ┴ ┴└─────────┘ └┘ ┴┴ ┴ ┴┴┴
src ┴└─────────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴└─────────┘ └┘ ┴┴ ┴ ┴┴┴
728
729 @[simp] lemma norm_algebra_map_eq {𝕜 : Type*} (𝕜' : Type*) [normed_field 𝕜] [normed_ring 𝕜']
id └──────────┘ ┴ └─────────┘ └┘
src └──────────┘ └─────────┘
typ └──────────┘ ┴ └─────────┘ └┘
doc └──┘ └──────────┘ └─────────┘
730 [h : normed_algebra 𝕜 𝕜'] (x : 𝕜) : ∥algebra_map 𝕜' x∥ = ∥x∥ :=
id └────────────┘ ┴ └┘ ┴ ┴└─────────┘ └┘ ┴┴ ┴ ┴┴┴
src └────────────┘ ┴└─────────┘ ┴ ┴ ┴ ┴
typ └────────────┘ ┴ └┘ ┴ ┴└─────────┘ └┘ ┴┴ ┴ ┴┴┴
doc └────────────┘
731 normed_algebra.norm_algebra_map_eq _ _
id └────────────────────────────────┘
src └────────────────────────────────┘
typ └────────────────────────────────┘
732
733 end normed_algebra
734
735 section restrict_scalars
736 set_option class.instance_max_depth 40
doc └──────────────────────┘
737
738 variables (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
id └──────────┘ └──────────┘ └────────────┘
src └──────────┘ └──────────┘ └────────────┘
typ └──────────┘ └──────────┘ └────────────┘
doc └──────────┘ └──────────┘ └────────────┘
739 {E : Type*} [normed_group E] [normed_space 𝕜' E]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
740
741 /-- `𝕜`-normed space structure induced by a `𝕜'`-normed space structure when `𝕜'` is a
742 normed algebra over `𝕜`. Not registered as an instance as `𝕜'` can not be inferred. -/
743 def normed_space.restrict_scalars : normed_space 𝕜 E :=
id └──────────┘ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴
doc └──────────┘
744 { norm_smul := λc x, begin
id ┴ ┴
typ ┴ ┴
st └─────
745 change ∥(algebra_map 𝕜' c) • x∥ = ∥c∥ * ∥x∥,
id ┴ └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘┴ └─────────┘┴ ┴ └┘┴┴ ┴┴┴┴ ┴┴┴
typ └─────┘┴ └─────────┘┴└┘┴ └┘┴┴ ┴┴┴┴ ┴ ┴┴┴ ┴
doc └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
746 simp [norm_smul]
id └───────┘
src └────┘└───────┘└─
typ └────┘└───────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st ─────────────────────
747 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
748 ..module.restrict_scalars 𝕜 𝕜' E }
id └─────────────────────┘ ┴ └┘ ┴
src └─────────────────────┘
typ └─────────────────────┘ ┴ └┘ ┴
doc └─────────────────────┘
749
750 end restrict_scalars
751
752 section summable
753 open_locale classical
754 open finset filter
755 variables [normed_group α] [complete_space α]
id ┴└──────────┘ └────────────┘
src └──────────┘ └────────────┘
typ ┴└──────────┘ └────────────┘
doc └──────────┘ └────────────┘
756
757 lemma summable_iff_vanishing_norm {f : ι → α} :
id ┴ ┴
typ ┴ ┴
758 summable f ↔ ∀ε > 0, ∃s:finset ι, ∀t, disjoint t s → ∥ t.sum f ∥ < ε :=
id └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴┴ ┴ └──────┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴ └────┘ ┴ └──────┘ ┴ └──┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴┴ ┴ └──────┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴
doc └──────┘ └────┘ └──────┘
759 begin
st └─────
760 simp only [summable_iff_vanishing, metric.mem_nhds_iff, exists_imp_distrib],
id └────────────────────┘ └─────────────────┘ └────────────────┘
src └─────────┘└────────────────────┘└┘└─────────────────┘└┘└────────────────┘┴
typ └─────────┘└────────────────────┘└┘└─────────────────┘└┘└────────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────────┘└─
761 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
762 { assume h ε hε, refine h {x | ∥x∥ < ε} ε hε _, rw [ball_0_eq ε] },
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───────┘ ┴
src └───────────┘ └─────┘ ┴┴└──┘┴ ┴┴┴┴ └┘ ┴ └┘ └──┘└───────┘┴ └┘
typ └───────────┘ └─────┘┴┴┴└──┘┴ ┴┴┴┴ └┘┴┴└┘└┘ └──┘└───────┘┴┴└┘
doc └───────────┘ └─────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └──┘ ┴ └┘
txt └───────────┘ └─────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └──┘ ┴ └┘
par └───────────┘ └─────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └──┘ ┴ └┘
pid └───────────┘ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └┘ ┴ ┴┴
st ───┘└───────────┘└─────────────────────────────┘└───────────────┘┴┴└┘└
763 { assume h s ε hε hs,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └────────────────┘
st ─────────────────────┘└─
764 rcases h ε hε with ⟨t, ht⟩,
id ┴ ┴ └┘
src └─────┘ ┴ ┴ └───────────┘
typ └─────┘┴┴┴┴└┘└───────────┘
doc └─────┘ ┴ ┴ └───────────┘
txt └─────┘ ┴ ┴ └───────────┘
par └─────┘ ┴ ┴ └───────────┘
pid ┴ ┴ ┴ └───────────┘
st ─────────────────────────────┘└─
765 refine ⟨t, assume u hu, hs _⟩,
id ┴ └┘
src └─────┘ └┘ └─────┘ └─┘
typ └─────┘ ┴└┘ └─────┘└┘└─┘
doc └─────┘ └┘ └─────┘ └─┘
txt └─────┘ └┘ └─────┘ └─┘
par └─────┘ └┘ └─────┘ └─┘
pid ┴ └┘ └─────┘ └─┘
st ────────────────────────────────┘└─
766 rw [ball_0_eq],
id └───────┘
src └──┘└───────┘┴
typ └──┘└───────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────┘└──
767 exact ht u hu }
id └┘ ┴ └┘
src └────┘ ┴ ┴ ┴
typ └────┘└┘┴┴┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────┘└─
768 end
st ──┘
769
770 lemma summable_of_norm_bounded {f : ι → α} (g : ι → ℝ) (hf : summable g) (h : ∀i, ∥f i∥ ≤ g i) :
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴
doc └──────┘
771 summable f :=
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
772 summable_iff_vanishing_norm.2 $ assume ε hε,
id └─────────────────────────┘┴ ┴ └┘
src └─────────────────────────┘┴
typ └─────────────────────────┘┴ ┴ └┘
773 let ⟨s, hs⟩ := summable_iff_vanishing_norm.1 hf ε hε in
id └─┘ ┴ └┘ └─────────────────────────┘┴ └┘ ┴ └┘
src └─────────────────────────┘┴
typ └─┘ ┴ └┘ └─────────────────────────┘┴ └┘ ┴ └┘
774 ⟨s, assume t ht,
id ┴ └┘
typ ┴ └┘
775 have ∥t.sum g∥ < ε := hs t ht,
id ┴┴└──┘ ┴┴ ┴ ┴ ┴ └┘
src ┴ └──┘ ┴ ┴
typ ┴┴└──┘ ┴┴ ┴ ┴ ┴ └┘
776 have nn : 0 ≤ t.sum g := finset.sum_nonneg (assume a _, le_trans (norm_nonneg _) (h a)),
id ┴ ┴└──┘ ┴ └───────────────┘ ┴ ┴ └──────┘ └─────────┘ ┴ ┴
src ┴ └──┘ └───────────────┘ └──────┘ └─────────┘
typ ┴ ┴└──┘ ┴ └───────────────┘ ┴ ┴ └──────┘ └─────────┘ ┴ ┴
777 lt_of_le_of_lt (norm_sum_le_of_le t (λ i _, h i)) $
id └────────────┘ └───────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────┘ └───────────────┘
typ └────────────┘ └───────────────┘ ┴ ┴ ┴ ┴ ┴
778 by rwa [real.norm_eq_abs, abs_of_nonneg nn] at this⟩
id └──────────────┘ └───────────┘ └┘
src └───┘└──────────────┘└┘└───────────┘┴ └───────┘
typ └───┘└──────────────┘└┘└───────────┘┴└┘└───────┘
doc └───┘ └┘ ┴ └───────┘
txt └───┘ └┘ ┴ └───────┘
par └───┘ └┘ ┴ └───────┘
pid └┘ └┘ ┴ ┴└──────┘
st └────────────────────┘└────────────────┘┴└──────┘
779
780 lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
id ┴ ┴ └──────┘ ┴ ┴┴ ┴┴ └──────┘ ┴
src └──────┘ ┴ ┴ └──────┘
typ ┴ ┴ └──────┘ ┴ ┴┴ ┴┴ └──────┘ ┴
doc └──────┘ └──────┘
781 summable_of_norm_bounded _ hf (assume i, le_refl _)
id └──────────────────────┘ └┘ ┴ └─────┘
src └──────────────────────┘ └─────┘
typ └──────────────────────┘ └┘ ┴ └─────┘
782
783 lemma norm_tsum_le_tsum_norm {f : ι → α} (hf : summable (λi, ∥f i∥)) : ∥(∑i, f i)∥ ≤ (∑ i, ∥f i∥) :=
id ┴ ┴ └──────┘ ┴ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴┴
src └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴┴ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴┴
doc └──────┘ ┴ ┴ ┴ ┴
784 have h₁ : tendsto (λs:finset ι, ∥s.sum f∥) at_top (𝓝 ∥(∑ i, f i)∥) :=
id └─────┘ └────┘ ┴ ┴┴└──┘ ┴┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────┘ └────┘ ┴ └──┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ └────┘ ┴ ┴┴└──┘ ┴┴ └────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └─────┘ └────┘ └────┘ ┴ ┴ ┴
785 (continuous_norm.tendsto _).comp (has_sum_tsum $ summable_of_summable_norm hf),
id └─────────────┘└──────┘ └──┘ └──────────┘ └───────────────────────┘ └┘
src └─────────────┘└──────┘ └──┘ └──────────┘ └───────────────────────┘
typ └─────────────┘└──────┘ └──┘ └──────────┘ └───────────────────────┘ └┘
786 have h₂ : tendsto (λs:finset ι, s.sum (λi, ∥f i∥)) at_top (𝓝 (∑ i, ∥f i∥)) :=
id └─────┘ └────┘ ┴ ┴└──┘ ┴ ┴┴ ┴┴ └────┘ ┴ ┴ ┴┴ ┴┴ ┴┴
src └─────┘ └────┘ └──┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ └────┘ ┴ ┴└──┘ ┴ ┴┴ ┴┴ └────┘ ┴ ┴ ┴┴ ┴┴ ┴┴
doc └─────┘ └────┘ └────┘ ┴ ┴ ┴
787 has_sum_tsum hf,
id └──────────┘ └┘
src └──────────┘
typ └──────────┘ └┘
788 le_of_tendsto_of_tendsto at_top_ne_bot h₁ h₂ $ univ_mem_sets' $ assume s, norm_sum_le _ _
id └──────────────────────┘ └───────────┘ └┘ └┘ └────────────┘ ┴ └─────────┘
src └──────────────────────┘ └───────────┘ └────────────┘ └─────────┘
typ └──────────────────────┘ └───────────┘ └┘ └┘ └────────────┘ ┴ └─────────┘
789
790 end summable